Towards Modern and Modular SAT for LCG

Lazy Clause Generation [31] is an architecture for building Constraint Programming solvers by making use of an underlying SAT engine [27]. LCG solvers such as Chuffed [10] and CP-SAT [32] define the state-of-the-art for constraint programming and have consistently scored the most points in the Free search category in the MiniZinc challenge ever since 2010 when one was first entered.

However, the SAT infrastructure used in LCG solvers is mainly based on SAT technology from at least a decade ago. Meanwhile, SAT solvers have made significant advances, including inprocessing [24], chronological backtracking [29], as well as improvement to search strategies by including local search components [9].

With these developments, it is worthwhile to investigate how a more modern conflict-driven clause learning (CDCL) SAT solver impacts the design choices of Lazy Clause Generation solvers. In this paper, we make use of the IPASIR-UP interface [15, 16] for extending SAT solvers and developing a new LCG solver. While the interface limits the design decisions, it also directly benefits from all the improvements of modern SAT solvers. As a result, it becomes necessary to revisit and reassess key decisions in LCG to determine how they are affected by these improvements.

In this short paper, we assume that the readers have a reasonable understanding of how both CP and SAT solvers work. For more details, see e.g. CP [33] and SAT [19].

LCG solvers aim to combine the high-level reasoning of CP solvers, allowing, for example, integer variables and global constraints, with the powerful conflict analysis of SAT solvers. The integration is possible by creating CP propagators that make their inference available to the SAT solver in clausal form. A key challenge is mapping the representation of finite domain/integer variables from the CP model to Booleans. The usual approach is to represent variables domains using both equality $[[x=d]]$ and bounds $[[x\ge d]]$ Booleans. Each time the LCG solver propagates, which is equivalent to setting one of these Booleans to true or false, it must be able to explain the propagation, by computing a clause which is a consequence of the CP model which will cause the propagation in the current solver state.

The first LCG solver [30] was built on top of MiniSAT 2.0$\beta$. Representation of integer variables was eager, creating both the bounds $[[x\ge d]]$ and equality $[[x=d]]$ literals for each integer $x$ before commencing search. The SAT solver controlled the search completely, and the CP engine was woken up once unit propagation ceased. This initial solver used clausal explanation, that is, when a propagator makes a new inference, it generated a clause that defined the propagation, and adds it to the SAT engine permanently. The new clauses then started more unit propagation in the SAT engine. This continued until failure was detected, and the SAT engine backjumped as usual, or a solution was found.

The next LCG architecture [17] reversed the control. Here the constraint programming engine was in control, performing search decisions. The unit propagation of clauses is treated as a (highest priority) propagator in the CP engine. The CP trail is extended with reason clauses for each propagation or failure, and conflict resolution works on the CP trail (in the usual CDCL manner). This architecture introduced lazy encoding, where equality literals were only created on demand, while bounds literals were created up front for integers $x$ with small initial domains, or lazily during search for integers with large initial domains. In this architecture, the explanation strategy was forward explanation, where each propagator built an explanation clause for each new propagation, at the time of propagation, but these explanation clauses only lived on the trail, and are removed when backjumping.

Chuffed [10] was built around a customized version of MiniSAT 2.2. It is extended to use a spaghetti stack, so it can insert into the stack for choicepoints earlier than the current choicepoint. It is much more similar to a SAT engine, with a propagation loop which runs when unit propagation quiesces. Again here explanation clauses only live in the trail, but propagators could implement forward explanation, or backwards explanation where the explanation clause is computed during conflict analysis, and not at propagation time. Chuffed did not implement propagators for many constraints, and instead encodes a number of constraints, such as element and table, into clauses.

After Chuffed was made open source in 2016, there has been a surge in LCG solvers. This might have been championed by the high-profile CP-SAT solver [32], developed as part of Google’s OR-Tools. This solver includes novel CP and SAT engines that implement some more modern SAT features, such as Glucose’s Literal Block Distance [3]. Other notable enhancements include the integration of a simplex based linear programming propagation [2], and a parallel portfolio approach of different variations of the solver, which makes the solver robust to different problem classes. At the same time, alternative solvers, such as Geas [22] and Pumpkin [12], have been developed by academics and have introduced exciting new features, such as core-guided search [21] and proof logging [20] for LCG.

A common trend among these new solvers is their tight integration and customization of the SAT solver employed. In the remainder of this paper, we will evaluate the opposite approach, where we maintain a clear boundary between the SAT and CP components, and the SAT solving is used without any customization.

The recent IPASIR-UP interface [15, 16] augments a conflict-driven clause learning (CDCL) SAT solver [27] with the capability to invoke and interact with an external propagation engine to improve the CDCL solver’s performance. The interface was originally implemented in the CaDiCaL solver [8] and successfully showcased in the setting of Satisfiability Modulo Theories (SMT) solving [4].

Although IPASIR-UP can be used to construct an LCG solver, it requires a change of perspective from the solver designer. Most LCG solvers use a SAT solver as a component to perform specific actions, such as clausal propagation and conflict resolution, within their search process. However, when using the IPASIR-UP interface, it is the SAT solver that runs the solving process, and it will make different calls to the external propagation engine at certain points in the process, much like the original LCG solver [30]. In our case, the external propagation engine will behave similarly to the CP component of most LCG solvers. It tracks the state of non-Boolean decision variables, such as integer variables, and oversees the running of propagators, which will communicate using literals and clauses.

Figure 1 shows the expected interactions between the SAT solver and our LCG engine. Hereinafter, when explaining the interplay between the SAT solver and the LCG backend, the names of the IPASIR-UP methods corresponding to the functionality being described are given in verbatim. The most important functionality of the IPASIR-UP interface is requesting external propagation. When this is required, the SAT solver will first notify the LCG backend of all literals that have been assigned since the last propagation (notify_assignments), and then ask it to propagate. To perform propagation, we maintain a priority queue of propagators that, given the new assignments, perform further inference [33]. We then activate the propagators in order until one performs any inference or the queue becomes empty. Propagators are required to inform the SAT engine about the outcome of their latest inference by providing literals that the SAT engine should assert (propagate) and clauses that can be added to the solver (add_external_clause). If no propagator performs any inference, then the LCG backend will report to be at fix point.

If the SAT solver performs conflict analysis that involves a literal inferred by the LCG backend, then the backend is expected to explain it by providing the corresponding antecedent clause (add_reason_clause). In the case of backward explanation, the backend reacts by computing such a clause and passing it to the solver. Otherwise, in the case of forward explanation, it constructs and stores all antecedent clauses during propagation and then emits them to the SAT solver upon such a request.

Explanations passed by the LCG backend to the SAT engine through IPASIR-UP are allowed to contain only literals known to the solver during search. This represents an obstacle if propagators’ literals are to be introduced lazily during backward explanation. This can, for example, prevent the strengthening of the explanation clauses through lifting, the process of generalizing an explanation. For example, given the constraint , we might infer that $x\le 1$ when $y\ge 1\wedge z\ge 1$; however, we can infer the same when $z\ge 0$. So instead, the lifted explanation could be $(y\ge 1\wedge z\ge 0)\to x\le 1$. The above requirement prevents us from introducing (and defining) new literals at this point. So if $z\ge 0$ was an already existing literal, then this lifting optimization would be possible. However, if it is a lazy literal to be introduced for the explanation, then it is not.

For an LCG backend, check_solution behaves largely the same as propagate, since its task is to check that no constraints are violated to validate the solution. A complication is that any higher level decision variables that introduce literals lazily, such as integer variables, might not yet be fixed to a single value. The most straightforward solution to this problem is to assume that the variables take a value in their domain (e.g. the lower bound), and check the constraints using these values. If no conflicts are found under these assumed values, then a solution is found (with the assumed values). Otherwise, the conflict detected will result in a new clause that can be used by the SAT solver for further propagation, which will ensure that the combination of assumed values that caused the conflict cannot be taken.

It is well known that the search strategy determined by the branching heuristic used can have an enormous impact on solving performance. Using the IPASIR-UP’s decide callback, the LCG backend can influence the search strategy. Most prominently, this method allows the backend to choose a literal to branch on. It can also be used to request the solver to restart, returning to a state where no decisions had been made. If no decision is made by the LCG backend, then the search strategy is left up to the SAT solver. Generally, it will make its decisions based on the variable state independent decaying sum (VSIDS) heuristic [28], and will use its own policy for restarts unless disabled.

Finally, the SAT solver is expected to inform the LCG backend of any changes to the decision level. It will inform the backend both when a new search decision level has been made (notify_new_decision_level) and when it backtracks to an earlier level (notify_backtrack). These notifications allow the LCG backend to maintain its own state that is reverted when backtracking. This can, for example, be used to maintain a state of which literals have been assigned and the current lower and upper bounds of integer variables.

We now introduce Huub [11], an open-source LCG solver implemented using the IPASIR-UP interface. We will use it to evaluate the performance of using modern SAT features and explore several design and engineering decisions for LCG solvers. The core engine of Huub is implemented in Rust 1.81.0 using CaDiCal 2.1.3 [8] as the back-end SAT solver, although in theory any SAT solver supporting the IPASIR-UP interface could be used. In the following experiments, the solver exercises through its FlatZinc interface. This allows us to use the MiniZinc Challenge [35] 2024 benchmarks, which consist of 20 problems with 5 instances each. Huub has propagators for all FlatZinc primitive constraints, but only supports the all_different and disjunctive global constraints. All other constraints are decomposed into these constraints or clauses using MiniZinc’s decompositions. All experiments were run on a single core of an Intel Xeon Gold 6338 processor with 16 GB and a 20-minute time limit.

We present Huub, an LCG solver built based on the IPASIR-UP interface to SAT engines. This modular design allows us to easily swap in any SAT solver that supports the interface, enabling the solver to benefit from the latest advancements in SAT solving technology. Our implementation demonstrates competitive performance compared to state-of-the-art LCG solvers, and we expect further improvements with more global constraint propagators.

As SAT solvers become more and more efficient in handling clauses, it is timely to revisit the design and engineering of LCG solvers. In this work, we investigate various explanation strategies and adaptive propagation techniques. In the future, we plan to explore other options, such as dynamically decomposing constraints and encoding them into the SAT solver on the fly [1].