Document Open Access Logo

Towards Modern and Modular SAT for LCG (Short Paper)

Authors Jip J. Dekker , Alexey Ignatiev , Peter J. Stuckey , Allen Z. Zhong

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CP.2025.42.pdf
  • Filesize: 0.7 MB
  • 12 pages
HTML5 Logo HTML (experimental)
LIPIcs.CP.2025.42.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Combinatorial optimization
Keywords
  • Lazy Clause Generation
  • Boolean Satisfiability
  • IPASIR-UP

Metrics

Abstract

Lazy Clause Generation (LCG) is an architecture for building Constraint Programming (CP) solvers using an underlying Boolean Satisfiability (SAT) engine. The CP propagation engine lazily creates clauses that define the integer variables and impose problem restrictions. The SAT engine uses the clausal model to reason and search, including, crucially, the generation of nogoods. However, while SAT solving has made significant advances recently, the underlying SAT technology in most LCG solvers has largely remained the same. Using a new interface to SAT engines, IPASIR-UP, we can construct an LCG solver which can swap out the underlying SAT engine with any that supports the interface. This new approach means we need to revisit many of the design and engineering decisions for LCG solvers, to take maximum advantage of a better underlying SAT engine while adhering to the restrictions of the interface. In this paper, we explore the possibilities and challenges of using IPASIR-UP for LCG, showing that it can be used to create a highly competitive solver.

Cite As Get BibTex

Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, and Allen Z. Zhong. Towards Modern and Modular SAT for LCG (Short Paper). In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 42:1-42:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CP.2025.42

Author Details

Jip J. Dekker
  • Department of Data Science and Artificial Intelligence, Monash University, Clayton, Australia
  • ARC Training Centre in Optimisation Technologies, Integrated Methodologies, and Applications (OPTIMA), Melbourne, Australia
Alexey Ignatiev
  • Department of Data Science and Artificial Intelligence, Monash University, Clayton, Australia
Peter J. Stuckey
  • Department of Data Science and Artificial Intelligence, Monash University, Clayton, Australia
  • ARC Training Centre in Optimisation Technologies, Integrated Methodologies, and Applications (OPTIMA), Melbourne, Australia
Allen Z. Zhong
  • Department of Data Science and Artificial Intelligence, Monash University, Clayton, Australia
  • ARC Training Centre in Optimisation Technologies, Integrated Methodologies, and Applications (OPTIMA), Melbourne, Australia

Funding

This research was partially funded by the Australian Government through the Australian Research Council Industrial Transformation Training Centre in Optimisation Technologies, Integrated Methodologies, and Applications (OPTIMA), Project ID IC200100009.

Supplementary Materials

References

  1. Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Peter J Stuckey. To encode or to propagate? the best choice for each constraint in SAT. In International Conference on Principles and Practice of Constraint Programming, pages 97-106. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40627-0_10.
  2. T Achterberg. Constraint integer programming. Ph. D. Thesis, Technische Universitat Berlin, 2007. Google Scholar
  3. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In Craig Boutilier, editor, IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009, pages 399-404, 2009. URL: http://ijcai.org/Proceedings/09/Papers/074.pdf.
  4. Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 1267-1329. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201017.
  5. Roberto J Bayardo and Biswanath Panda. Fast algorithms for finding extremal sets. In Proceedings of the 2011 SIAM International Conference on Data Mining, pages 25-34. SIAM, 2011. URL: https://doi.org/10.1137/1.9781611972818.3.
  6. Nicolas Beldiceanu, Qi Guo, and Sven Thiel. Non-overlapping constraints between convex polytopes. In International Conference on Principles and Practice of Constraint Programming, pages 392-407. Springer, 2001. URL: https://doi.org/10.1007/3-540-45578-7_27.
  7. Armin Biere. Adaptive restart strategies for conflict driven SAT solvers. In Hans Kleine Büning and Xishun Zhao, editors, Theory and Applications of Satisfiability Testing - SAT 2008, 11th International Conference, SAT 2008, Guangzhou, China, May 12-15, 2008. Proceedings, volume 4996 of Lecture Notes in Computer Science, pages 28-33. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-79719-7_4.
  8. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1, pages 51-53, 2020. Google Scholar
  9. Shaowei Cai and Xindi Zhang. Deep cooperation of CDCL and local search for sat. In Theory and Applications of Satisfiability Testing-SAT 2021: 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings 24, pages 64-81. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_6.
  10. Geoffrey Chu. Improving combinatorial optimization. PhD thesis, Department of Computing and Information Systems, University of Melbourne, 2011. Google Scholar
  11. Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, and Allen Z. Zhong. Huub: Lazy Clause Generation Solver. Software, (visited on 2025-07-24). URL: https://github.com/huub-solver/huub
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.24103
  12. Emir Demirović, Maarten Flippo, Imko Marijnissen, Jeff Smits, and Konstantin Sidorov. Pumpkin Solver. URL: https://github.com/ConSol-Lab/Pumpkin.
  13. Niklas Eén and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In International conference on theory and applications of satisfiability testing, pages 61-75. Springer, 2005. URL: https://doi.org/10.1007/11499107_5.
  14. Katalin Fazekas, Armin Biere, and Christoph Scholl. Incremental inprocessing in SAT solving. In Theory and Applications of Satisfiability Testing-SAT 2019: 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings 22, pages 136-154. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_9.
  15. Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. IPASIR-UP: user propagators for CDCL. In SAT, volume 271 of LIPIcs, pages 8:1-8:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.8.
  16. Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. Satisfiability modulo user propagators. Journal of Artificial Intelligence Research, 81:989-1017, 2024. URL: https://doi.org/10.1613/JAIR.1.16163.
  17. T. Feydy and P.J. Stuckey. Lazy clause generation reengineered. In I. Gent, editor, Proceedings of the 15th International Conference on Principles and Practice of Constraint Programming, volume 5732 of LNCS, pages 352-366. Springer-Verlag, 2009. URL: https://doi.org/10.1007/978-3-642-04244-7_29.
  18. Thibaut Feydy, Andreas Schutt, and Peter J Stuckey. Global difference constraint propagation for finite domain solvers. In Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pages 226-235, 2008. URL: https://doi.org/10.1145/1389449.1389478.
  19. Johannes K. Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. The silent (r)evolution of sat. Communication of the ACM, 66(6):64-72, May 2023. URL: https://doi.org/10.1145/3560469.
  20. Maarten Flippo, Konstantin Sidorov, Imko Marijnissen, Jeff Smits, and Emir Demirovic. A multi-stage proof logging framework to certify the correctness of CP solvers. In Paul Shaw, editor, 30th International Conference on Principles and Practice of Constraint Programming, CP 2024, September 2-6, 2024, Girona, Spain, volume 307 of LIPIcs, pages 11:1-11:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.CP.2024.11.
  21. Graeme Gange, Jeremias Berg, Emir Demirović, and Peter J Stuckey. Core-guided and core-boosted search for CP. In Integration of Constraint Programming, Artificial Intelligence, and Operations Research: 17th International Conference, CPAIOR 2020, Vienna, Austria, September 21-24, 2020, Proceedings 17, pages 205-221. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58942-4_14.
  22. Graeme Gange, Daniel Harabor, and Peter J. Stuckey. Lazy CBS: Implicit conflict-based search using lazy clause generation. In Nir Lipovetzky, Eva Onaindia, and David Smith, editors, Proceedings of the 29th International Conference on Automated Planning and Scheduling, pages 155-162. AAAI Press, 2019. URL: https://www.aaai.org/ojs/index.php/ICAPS/article/view/3471.
  23. Alexey Ignatiev, Zi Li Tan, and Christos Karamanos. Towards universally accessible sat technology. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024), pages 16-1. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. Google Scholar
  24. Matti Järvisalo, Marijn JH Heule, and Armin Biere. Inprocessing rules. In International Joint Conference on Automated Reasoning, pages 355-370. Springer, 2012. Google Scholar
  25. Benjamin Kiesl, Marijn J. H. Heule, and Armin Biere. Truth assignments as conditional autarkies. In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, volume 11781 of Lecture Notes in Computer Science, pages 48-64. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_3.
  26. Inês Lynce and Joao Marques-Silva. Probing-based preprocessing techniques for propositional satisfiability. In Proceedings. 15th IEEE International Conference on Tools with Artificial Intelligence, pages 105-110. IEEE, 2003. Google Scholar
  27. Joao Marques-Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 133-182. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200987.
  28. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In DAC, pages 530-535. ACM, 2001. URL: https://doi.org/10.1145/378239.379017.
  29. Alexander Nadel and Vadim Ryvchin. Chronological backtracking. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018, pages 111-121, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-94144-8_7.
  30. O. Ohrimenko, P.J. Stuckey, and M. Codish. Propagation = lazy clause generation. In C. Bessiere, editor, Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming, volume 4741 of LNCS, pages 544-558. Springer-Verlag, 2007. URL: https://doi.org/10.1007/978-3-540-74970-7_39.
  31. O. Ohrimenko, P.J. Stuckey, and M. Codish. Propagation via lazy clause generation. Constraints, 14(3):357-391, 2009. URL: https://doi.org/10.1007/S10601-008-9064-X.
  32. Laurent Perron and Frédéric Didier. CP-SAT. URL: https://developers.google.com/optimization/cp/cp_solver/.
  33. Christian Schulte and Peter J. Stuckey. Efficient constraint propagation engines. ACM Trans. Program. Lang. Syst., 31(1):2:1-2:43, 2008. URL: https://doi.org/10.1145/1452044.1452046.
  34. Andreas Schutt, Thibaut Feydy, Peter J Stuckey, and Mark G Wallace. Explaining the cumulative propagator. Constraints, 16:250-282, 2011. URL: https://doi.org/10.1007/S10601-010-9103-2.
  35. Peter J Stuckey, Ralph Becket, and Julien Fischer. Philosophy of the MiniZinc challenge. Constraints, 15:307-316, 2010. URL: https://doi.org/10.1007/S10601-010-9093-0.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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