2026-07-20T05:25:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23903 2025-11-12T13:11:16Z ddc:004 open_access

Towards Modern and Modular SAT for LCG (Short Paper) Dekker, Jip J. Ignatiev, Alexey Stuckey, Peter J. Zhong, Allen Z. Lazy Clause Generation Boolean Satisfiability IPASIR-UP 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jip J. Dekker and Alexey Ignatiev and Peter J. Stuckey and Allen Z. Zhong 2025 Is Part Of LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2025.42 urn:nbn:de:0030-drops-239038 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.42 eng https://creativecommons.org/licenses/by/4.0/legalcode