Document Open Access Logo

Structure-Guided Local Improvement for Maximum Satisfiability

Authors André Schidler , Stefan Szeider

PDF

File

Thumbnail PDF
PDF
LIPIcs.CP.2024.26.pdf
  • Filesize: 0.73 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Hardware → Theorem proving and SAT solving
  • Theory of computation → Discrete optimization
  • Theory of computation → Automated reasoning
  • Theory of computation → Constraint and logic programming
  • General and reference → Experimentation
Keywords
  • maximum satisfiability
  • large neighborhood search (LNS)
  • SAT-based local improvement (SLIM)
  • incomplete MaxSAT
  • graphical structure
  • metaheuristic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

The enhanced performance of today’s MaxSAT solvers has elevated their appeal for many large-scale applications, notably in software analysis and computer-aided design. Our research delves into refining anytime MaxSAT solving by repeatedly identifying and solving with an exact solver smaller subinstances that are chosen based on the graphical structure of the instance. We investigate various strategies to pinpoint these subinstances. This structure-guided selection of subinstances provides an exact solver with a high potential for improving the current solution. Our exhaustive experimental analyses contrast our methodology as instantiated in our tool MaxSLIM with previous studies and benchmark it against leading-edge MaxSAT solvers.

Cite As Get BibTex

André Schidler and Stefan Szeider. Structure-Guided Local Improvement for Maximum Satisfiability. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 26:1-26:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CP.2024.26

Author Details

André Schidler
  • Algorithms and Complexity Group, TU Wien, Austria
Stefan Szeider
  • Algorithms and Complexity Group, TU Wien, Austria

Funding

Austrian Science Fund (FWF), project 10.55776/P36420.

Acknowledgements

Part of this work was carried out while taking part in the Dagstuhl Seminar 23261 "SAT Encodings and Beyond," as well as in the extended reunion of the program "Satisfiability: Theory, Practice, and Beyond" in the spring of 2023 at the Simons Institute for the Theory of Computing at UC Berkeley.

Supplementary Materials

References

  1. Benjamin Andres, Benjamin Kaufmann, Oliver Matheis, and Torsten Schaub. Unsatisfiability-based optimization in clasp. In Agostino Dovier and Vítor Santos Costa, editors, Technical Communications of the 28th International Conference on Logic Programming, ICLP 2012, September 4-8, 2012, Budapest, Hungary, volume 17 of LIPIcs, pages 211-221. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.ICLP.2012.211.
  2. Carlos Ansótegui, Maria Luisa Bonet, Joel Gabàs, and Jordi Levy. Improving sat-based weighted maxsat solvers. In Michela Milano, editor, Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012. Proceedings, volume 7514 of Lecture Notes in Computer Science, pages 86-101. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33558-7_9.
  3. Carlos Ansótegui, Josep Pon, Meinolf Sellmann, and Kevin Tierney. Reactive dialectic search portfolios for MaxSAT. In Satinder Singh and Shaul Markovitch, editors, Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, February 4-9, 2017, San Francisco, California, USA, pages 765-772. AAAI Press, 2017. URL: http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14872.
  4. Jeremias Berg, Emir Demirovic, and Peter J. Stuckey. Core-boosted linear search for incomplete MaxSAT. In Louis-Martin Rousseau and Kostas Stergiou, editors, Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 16th International Conference, CPAIOR 2019, Thessaloniki, Greece, June 4-7, 2019, Proceedings, volume 11494 of Lecture Notes in Computer Science, pages 39-56. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-19212-9_3.
  5. Jeremias Berg, Matti Järvisalo, Ruben Martins, and Andreas Niskanen. Maxsat evaluation 2023: Solver and benchmark descriptions. Technical report, University of Helsinki, 2023. Google Scholar
  6. Shaowei Cai and Zhendong Lei. Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability. Artif. Intell., 287:103354, 2020. URL: https://doi.org/10.1016/J.ARTINT.2020.103354.
  7. Yi Chu, Shaowei Cai, and Chuan Luo. NuWLS: improving local search for (weighted) partial MaxSAT by new weighting techniques. In Brian Williams, Yiling Chen, and Jennifer Neville, editors, Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023, pages 3915-3923. AAAI Press, 2023. URL: https://ojs.aaai.org/index.php/AAAI/article/view/25505.
  8. Aviad Cohen, Alexander Nadel, and Vadim Ryvchin. Local search with a SAT oracle for combinatorial optimization. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, volume 12652 of Lecture Notes in Computer Science, pages 87-104. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_5.
  9. Emir Demirovic and Nysret Musliu. MaxSAT-based large neighborhood search for high school timetabling. Comput. Oper. Res., 78:172-180, 2017. URL: https://doi.org/10.1016/j.cor.2016.08.004.
  10. Yu Feng, Osbert Bastani, Ruben Martins, Isil Dillig, and Saswat Anand. Automated synthesis of semantic malware signatures using maximum satisfiability. In 24th Annual Network and Distributed System Security Symposium, NDSS 2017, San Diego, California, USA, February 26 - March 1, 2017. The Internet Society, 2017. URL: https://www.ndss-symposium.org/ndss2017/ndss-2017-programme/automated-synthesis-semantic-malware-signatures-using-maximum-satisfiability/.
  11. Johannes K. Fichte, Neha Lodha, and Stefan Szeider. SAT-based local improvement for finding tree decompositions of small width. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10491 of Lecture Notes in Computer Science, pages 401-411. Springer Verlag, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_25.
  12. Randy Hickey and Fahiem Bacchus. Large neighbourhood search for anytime MaxSAT solving. In Lud De Raedt, editor, Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22, pages 1818-1824. International Joint Conferences on Artificial Intelligence Organization, July 2022. URL: https://doi.org/10.24963/ijcai.2022/253.
  13. Sepideh Khoshnood, Markus Kusano, and Chao Wang. ConcBugAssist: constraint solving for diagnosis and repair of concurrency bugs. In Michal Young and Tao Xie, editors, Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015, Baltimore, MD, USA, July 12-17, 2015, pages 165-176. ACM, 2015. URL: https://doi.org/10.1145/2771783.2771798.
  14. Alexander S. Kulikov, Danila Pechenev, and Nikita Slezkin. SAT-based circuit local improvement. In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors, 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria, volume 241 of LIPIcs, pages 67:1-67:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.67.
  15. Neha Lodha, Sebastian Ordyniak, and Stefan Szeider. A SAT approach to branchwidth. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 179-195. Springer Verlag, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_12.
  16. Neha Lodha, Sebastian Ordyniak, and Stefan Szeider. SAT-encodings for special treewidth and pathwidth. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10491 of Lecture Notes in Computer Science, pages 429-445. Springer Verlag, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_27.
  17. João Marques-Silva, Josep Argelich, Ana Graça, and Inês Lynce. Boolean lexicographic optimization: algorithms & applications. Ann. Math. Artif. Intell., 62(3-4):317-343, 2011. URL: https://doi.org/10.1007/S10472-011-9233-2.
  18. Ruben Martins, Vasco M. Manquinho, and Inês Lynce. Open-WBO: A modular MaxSAT solver,. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of Lecture Notes in Computer Science, pages 438-445. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_33.
  19. António Morgado, Carmine Dodaro, and João Marques-Silva. Core-guided MaxSAT with soft cardinality constraints. In Barry O'Sullivan, editor, Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, Lyon, France, September 8-12, 2014. Proceedings, volume 8656 of Lecture Notes in Computer Science, pages 564-573. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-10428-7_41.
  20. António Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, and João Marques-Silva. Iterative and core-guided maxsat solving: A survey and assessment. Constraints An Int. J., 18(4):478-534, 2013. URL: https://doi.org/10.1007/s10601-013-9146-2.
  21. Alexander Nadel. Solving MaxSAT with bit-vector optimization. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 54-72. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_4.
  22. Alexander Nadel. Anytime weighted MaxSAT with improved polarity selection and bit-vector optimization. In Clark W. Barrett and Jin Yang, editors, 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019, pages 193-202. IEEE, 2019. URL: https://doi.org/10.23919/FMCAD.2019.8894273.
  23. Alexander Nadel. On optimizing a generic function in SAT. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, pages 205-213. IEEE, 2020. URL: https://doi.org/10.34727/2020/ISBN.978-3-85448-042-6_28.
  24. Alexander Nadel. Polarity and variable selection heuristics for sat-based anytime maxsat. J. Satisf. Boolean Model. Comput., 12(1):17-22, 2020. URL: https://doi.org/10.3233/sat-200126.
  25. David Pisinger and Stefan Ropke. Large neighborhood search. In Handbook of Metaheuristics, pages 399-419. Springer Verlag, 2010. Google Scholar
  26. Vaidyanathan Peruvemba Ramaswamy and Stefan Szeider. MaxSAT-based postprocessing for treedepth. In Helmut Simonis, editor, Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedings, volume 12333 of Lecture Notes in Computer Science, pages 478-495. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_28.
  27. Vaidyanathan Peruvemba Ramaswamy and Stefan Szeider. Learning fast-inference bayesian networks. In Marc'Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan, editors, Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual, pages 17852-17863, 2021. URL: https://proceedings.neurips.cc/paper/2021/hash/94e70705efae423efda1088614128d0b-Abstract.html.
  28. Vaidyanathan Peruvemba Ramaswamy and Stefan Szeider. Turbocharging treewidth-bounded bayesian network structure learning. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021, pages 3895-3903. AAAI Press, 2021. URL: https://doi.org/10.1609/aaai.v35i5.16508.
  29. Vaidyanathan Peruvemba Ramaswamy and Stefan Szeider. Learning large Bayesian networks with expert constraints. In James Cussens and Kun Zhang, editors, Proceedings of the Thirty-Eighth Conference on Uncertainty in Artificial Intelligence, volume 180 of Proceedings of Machine Learning Research, pages 1592-1601. PMLR, 01-05 August 2022. URL: https://proceedings.mlr.press/v180/peruvemba-ramaswamy22a.html.
  30. Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider. Circuit minimization with QBF-based exact synthesis. In Brian Williams, Yiling Chen, and Jennifer Neville, editors, Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023, pages 4087-4094. AAAI Press, 2023. URL: https://ojs.aaai.org/index.php/AAAI/article/view/25524.
  31. Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider. eSLIM: Circuit minimization with SAT based local improvement. In 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, August 21-24, 2024, Pune, India, 2024. to appear. Google Scholar
  32. André Schidler. SAT-based local search for plane subgraph partitions (CG challenge). In Xavier Goaoc and Michael Kerber, editors, 38th International Symposium on Computational Geometry, SoCG 2022, June 7-10, 2022, Berlin, Germany, volume 224 of LIPIcs, pages 74:1-74:8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SoCG.2022.74.
  33. André Schidler and Stefan Szeider. SAT-based decision tree learning for large data sets. In Proceedings of AAAI'21, the Thirty-Fifth AAAI Conference on Artificial Intelligence. AAAI Press, 2021. URL: https://doi.org/10.1609/aaai.v35i5.16509.
  34. André Schidler and Stefan Szeider. SAT-boosted tabu search for coloring massive graphs. ACM J. Exp. Algorithmics, 28, July 2023. URL: https://doi.org/10.1145/3603112.
  35. André Schidler and Stefan Szeider. SAT-based decision tree learning for large data sets. J. Artif. Intell. Res., 80:875-918, 2024. Google Scholar
  36. Paul Shaw. Using constraint programming and local search methods to solve vehicle routing problems. In Michael J. Maher and Jean-Francois Puget, editors, Principles and Practice of Constraint Programming - CP98, 4th International Conference, Pisa, Italy, October 26-30, 1998, Proceedings, volume 1520 of Lecture Notes in Computer Science, pages 417-431. Springer, 1998. URL: https://doi.org/10.1007/3-540-49481-2_30.
  37. Xujie Si, Xin Zhang, Radu Grigore, and Mayur Naik. Maximum satisfiability in software analysis: Applications and techniques. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, volume 10426 of Lecture Notes in Computer Science, pages 68-94. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63387-9_4.
  38. Charlie Shucheng Zhu, Georg Weissenbacher, Divjyot Sethi, and Sharad Malik. Sat-based techniques for determining backbones for post-silicon fault localisation. In Zeljko Zilic and Sandeep K. Shukla, editors, 2011 IEEE International High Level Design Validation and Test Workshop, HLDVT 2011, Napa Valley, CA, USA, November 9-11, 2011, pages 84-91. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/HLDVT.2011.6113981.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact