A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

The Sledgehammer subsystem [7, 48] integrates automatic theorem provers in Isabelle/HOL, including CVC4, E, LEO-II, Satallax, SPASS, Vampire, veriT, and Z3. Upon invocation, it heuristically selects relevant lemmas from the thousands available in loaded libraries, translates them along with the current proof obligation to SMT-LIB or TPTP, and invokes the automatic provers. In case of success, the machine-generated proof is translated to an Isar proof that can be inserted into the formal development, so that the external provers do not need to be trusted.

Sledgehammer is part of most Isabelle users’ workflow, and we invoke it dozens of times a day (according to the log files it produces). For example, while formalizing some results that depend on multisets, we found ourselves needing the basic property

where A and B are finite multisets, \(\cup \) denotes union defined such that for each element x, the multiplicity of x in \(A \cup B\) is the maximum of the multiplicities of x in A and B, \(\cap \) denotes intersection, and denotes cardinality. This lemma was not available in Isabelle’s underdeveloped multiset library, so we invoked Sledgehammer. Within 30 s, the tool came back with a brief proof text invoking a suitable tactic with a list of ten lemmas from the library, which we could insert into our formalization:

The generated proof refers to 10 library lemmas by name and applies the metis search tactic.

Without Sledgehammer, proving the above property could easily have taken 5–15 min. A manual proof, expressed in Isar’s declarative style, might look like this:

The function returns the multiplicity of an element in a multiset. The \(\uplus \) operator denotes the disjoint union operation—for each element, it computes the sum of the multiplicities in the operands (as opposed to the maximum for \(\cup \)).

In Isar proofs, intermediate properties are introduced using and proved using a tactic such as simp and auto. Proof blocks ( \(\;\ldots \;\) ) can be nested. The advantage of Isar proofs over one-line metis proofs is that we can follow and understand the steps. However, for lemmas about multisets and other background theories, we are usually content if we can get a proof automatic and carry on with formalizing the more interesting foreground theory.

Isabelle locales are a convenient mechanism for structuring large proofs. A locale fixes types, constants, and assumptions within a specified scope. A schematic example follows:

The definition of locale implicitly fixes a type , explicitly fixes a constant whose type may depend on , and states an assumption over and  . Definitions made within the locale may depend on and , and lemmas proved within the locale may additionally depend on . A single locale can introduce several types, constants, and assumptions. Seen from the outside, the lemmas proved in are polymorphic in type variable , universally quantified over , and conditional on .

Locales support inheritance, union, and embedding. To embed into , or make a sublocale of , we must recast an instance of into an instance of , by providing, in the context of , definitions of the types and constants of together with proofs of ’s assumptions. The command

emits the proof obligation , where \(\upsilon \) and may depend on types and constants available in . After the proof, all the lemmas proved in become available in , with and  instantiated with \(\upsilon \) and  .

The Refinement Framework [30] provides definitions, lemmas, and tools that assist in the verification of functional and imperative programs via stepwise refinement [59]. The framework defines a programming language that is built on top of a nondeterminism monad. A program is a function that returns an object of type :

The Isabelle syntax is similar to that of Standard ML and other typed functional programming languages: The type is freely generated by its two constructors, and . The set X in specifies the possible values that can be returned. The return statement is defined as a constant and specifies a single value, whereas indicates that an unspecified positive number is returned. The simplest program is a semantic specification of the possible outputs, encapsulated in a constructor. The following example is a nonexecutable specification of the function that subtracts 1 from every element of the list (with \(0 - 1\) defined as 0 on natural numbers):

Program refinement uses the same source and target language. The refinement relation \(\le \) is defined by and for all r. For example, the concrete program refines (\(\le \)) the abstract program , meaning that all concrete behaviors are possible in the abstract version. The bottom element is an unrefinable program; the top element represents a run-time failure (e.g., a failed assertion) or divergence.

Refinement can be used to change the program’s data structures and algorithms, towards a more deterministic and usually more efficient program for which executable code can be generated. For example, we can refine the previous specification to a program that uses a ‘while’ loop:

The program relies on the following constructs:To prove the refinement lemma , we can use the refine_vcg proof method provided by the Refinement Framework. This method heuristically aligns the statements of the two programs and generates proof obligations, which are passed to the user. If the abstract program has the form or , as is the case here, refine_vcg applies Hoare-logic-style rules to generate the verification conditions. For our example, two of the resulting proof obligations correspond to the termination of the ‘while’ loop and the correctness of the assertion. We can use the measure to prove termination.

In a refinement step, we can also change the types. For our small program, if we assume that the natural numbers in the list are all nonzero, we can replace them by integers and use the subtraction operation on integers (for which \(0 - 1 = -1 \not = 0\)). The program remains syntactically identical except for the type annotation:

We want to establish the following relation: If all elements in are nonzero and the elements of are positionwise numerically equal to those of , then any list of integers returned by is positionwise numerically equal to some list returned by . The framework lets us express preconditions and connections between types using higher-order relations called relators:

The relation relates natural numbers with their integer counterparts (e.g., ). The syntax of relators mimics that of types; for example, if R is the relation for , then is the relation for , and is the relation for . The ternary relator \([p]\,R \rightarrow S\), for functions , lifts the relations R and S for and under precondition p.

The Imperative HOL library [14] defines a heap monad that can express imperative programs with side effects. On top of Imperative HOL, a separation logic, with assertion type , can be used to express relations between plain values, of type , and data structures on the heap, of type . For example, relates lists of elements with mutable arrays of elements, where is used to relate the elements. The relation between the ! operator on lists and its heap-based counterpart can be expressed as follows:

The arguments’ relations are annotated with \(^{\mathrm {k}}\) (“keep”) or \(^{\mathrm {d}}\) (“destroy”) superscripts that indicate whether the previous value can still be accessed after the operation has been performed. Reading an array leaves it unchanged, whereas updating it destroys the old array.

The following command generates a heap program called from the source program :

The generated array-based program is

The end-to-end refinement theorem, obtained by composing the refinement lemmas, is

If we want to execute the program efficiently, we can translate it to Standard ML using Isabelle’s code generator [23]. The following imperative code, including its dependencies, is generated (in slightly altered form):

×

The ML idiom \(\texttt {(fn () => \ldots ) ()}\) is inserted to delay the evaluation of the body, so that the side effects occur in the intended order.

The DPLL and CDCL calculi distinguish between literals whose truth value has been decided arbitrarily and those that are entailed by the current decisions; for the latter, it is sometimes useful to know which clause entails it. To capture this information, we introduce a type of annotated literals, parameterized by a type of propositional variables and a type of clauses:

The simpler calculi do not use ; they take , a singleton type whose unique value is (). Informally, we write A, \(\lnot \,A\), and \(L^\dag \) for positive, negative, and decision literals, and we write \(L^C\) (with ) or simply L (if or if the clause C is irrelevant) for propagated literals. The unary minus operator is used to negate a literal, with \(- (\lnot \,A) = A\).

As is customary in the literature [1, 57], clauses are represented by multisets, ignoring the order of literals but not repetitions. A is a (finite) multiset over . Clauses are often stored in sets or multisets of clauses. To ease reading, we write clauses using logical symbols (e.g., \(\bot \), L, and \(C \vee D\) for \(\emptyset \), \(\{L\}\), and \(C \uplus D\)). Given a clause C, we write \(\lnot \,C\) for the formula that corresponds to the clause’s negation.

Given a set or multiset I of literals, \(I \vDash C\) is true if and only if C and I share a literal. This is lifted to sets and multisets of clauses or formulas: . A set or multiset is satisfiable if there exists a consistent set or multiset of literals I such that \(I \vDash N\). Finally, These notations are also extended to formulas.

Nieuwenhuis et al. present CDCL as a set of transition rules on states. A state is a pair , where M is the trail and N is the multiset of clauses to satisfy. In a slight abuse of terminology, we will refer to the multiset of clauses as the “clause set.” The trail is a list of annotated literals that represents the partial model under construction. The empty list is written . Somewhat nonstandardly, but in accordance with Isabelle conventions for lists, the trail grows on the left: Adding a literal L to M results in the new trail \(L \cdot M\), where . The concatenation of two lists is written \(M \mathbin {@} M'\). To lighten the notation, we often build lists from elements and other lists by simple juxtaposition, writing \(M L M'\) for \(M \mathbin {@} L \cdot M'\).

The core of the CDCL calculus is defined as a transition relation , an extension of classical DPLL [17] with nonchronological backtracking, or backjumping. The part of the name refers to Nieuwenhuis, Oliveras, and Tinelli. The calculus consists of three rules, starting from an initial state . In the following, we abuse notation, implicitly converting \(\vDash \)’s first operand from a list to a set and ignoring annotations on literals:The rule is more general than necessary for capturing DPLL, where it suffices to negate the leftmost decision literal. The general rule can also express nonchronological backjumping, if \(C'\vee L'\) is a new clause derived from N (but not necessarily in N).

We represented the calculus as an inductive predicate. For the sake of modularity, we formalized the rules individually as their own predicates and combined them to obtain :

Since there is no call to in the assumptions, we could also have used a plain here, but the command provides convenient introduction and elimination rules. The predicate operates on states of type . To allow for refinements, this type is kept as a parameter of the calculus, using a locale that abstracts over it and that provides basic operations to manipulate states:

where converts an abstract state of type to a pair (M, N). Inside the locale, states are compared extensionally: is true if the two states have identical trails and clause sets (i.e., if ). This comparison ignores any other fields that may be present in concrete instantiations of the abstract state type .

Each calculus rule is defined in its own locale, based on and parameterized by additional side conditions. Complex calculi are built by inheriting and instantiating locales providing the desired rules. For example, the following locale provides the predicate corresponding to the rule, phrased in terms of an abstract DPLL state:

Following a common idiom, the calculus is distributed over two locales: The first locale, , defines the calculus; the second locale, , extends it with an assumption expressing a structural invariant over that is instantiated when proving concrete properties later. This cannot be achieved with a single locale, because definitions may not precede assumptions.

Termination is proved by exhibiting a well-founded relation \(\prec \) such that whenever . Let and with the decompositionswhere the trail segments \(M_0,\ldots ,M_n,M'_0,\ldots ,M'_{n\smash {'}}\) contain no decision literals. Let V be the number of distinct variables occurring in the initial clause set N. Now, let \(\nu \,M = V - \left| M\right| \), indicating the number of unassigned variables in the trail M. Nieuwenhuis et al. define \(\prec \) such that ifThis order is not to be confused with the lexicographic order: We have by condition (2), whereas . Yet the authors justify well-foundedness by appealing to the well-foundedness of on bounded lists over finite alphabets. In our proof, we clarify and simplify matters by mapping states to lists \(\bigl [\left| M_0\right| , \cdots ,\left| M_n\right| \bigr ]\), without appealing to \(\nu \). Using the standard lexicographic order, states become larger with each transition:

The lists corresponding to possible states are bounded by the list \([V, \dots , V]\) consisting of V occurrences of V,  thereby delimiting a finite domain \(D = \{[k_1,\ldots ,k_n] \mid k_1,\cdots ,k_n,n \le V\}\). We take \(\prec \) to be the restriction of to D. A variant of this approach is to encode lists into a measure and let , building on the well-foundedness of > over bounded sets of natural numbers.

A final state is a state from which no transitions are possible. Given a relation , we write for the right-restriction of its reflexive transitive closure to final states (i.e., if and only if ).

We first prove structural invariants on arbitrary states reachable from , namely: (1) each variable occurs at most once in \(M'\); (2) if \(M' = M_2 L M_1\) where L is propagated, then \(M_1, N \vDash L\). From these invariants, together with the constraint that is a final state, it is easy to prove the theorem.

The locale machinery allows us to derive a classical DPLL calculus from DPLL with backjumping. We call this calculus . It is achieved through a locale that restricts the Backjump rule so that it performs only chronological backtracking:Because of the locale parameters, is strictly speaking a family of calculi.

The rule depends on two clauses: a conflict clause C and a clause \(C'\vee L'\) that justifies the propagation of \(L'\!.\) The conflict clause is specified by . As for \(C'\vee L'\), given a trail \(M'L^\dag M\) decomposable as \(M_nL^\dag M_{n-1}L_{n\smash {-1}}^\dag \cdots M_1 L_1^ \dag M_0\) where \(M_0,\cdots ,M_n\) contain no decision literals, we can take \(C' = -L_1\vee \cdots \vee -L_{n-1}\).

Consequently, the inclusion holds. In Isabelle, this is expressed as a locale instantiation: is made a sublocale of , with a side condition restricting the application of the rule. The partial correctness and termination theorems are inherited from the base locale. instantiates the abstract state type with a concrete type of pairs. By discharging the locale assumptions emerging with the command, we also verify that these assumptions are consistent. Roughly:

If a conflict cannot be resolved by backtracking, we would like to have the option of stopping even if some variables are undefined. A state is conclusive if \(M \vDash N\) or if N contains a conflicting clause and M contains no decision literals. For , all final states are conclusive, but not all conclusive states are final.

The theorem does not require stopping at the first conclusive state. In an implementation, testing \(M\vDash N\) can be expensive, so a solver might fail to notice that a state is conclusive and continue for some time. In the worst case, it will stop in a final state—which is guaranteed to exist by Theorem 1. In practice, instead of testing whether \(M\vDash N\), implementations typically apply the rules until every literal is set. When N is satisfiable, this produces a total model.

The abstract CDCL calculus extends with a pair of rules for learning new lemmas and forgetting old ones:In practice, the rule is normally applied to clauses built exclusively from atoms in M, because the learned clause is false in M. This property eventually guarantees that the learned clause is not redundant (e.g., it is not already contained in N).

We call this calculus . In general, does not terminate, because it is possible to learn and forget the same clause infinitely often. But for some instantiations of the parameters with suitable restrictions on and , the calculus always terminates.

In many SAT solvers, the only clauses that are ever learned are the ones used for backtracking. If we restrict the learning so that it is always done immediately before backjumping, we can be sure that some progress will be made between a and the next or . This idea is captured by the following combined rule:The calculus variant that performs this rule instead of and is called . Because a single transition corresponds to two transitions in , the inclusion does not hold. Instead, we have . Each step of corresponds to a single step in or a two-step sequence consisting of followed by .

Modern SAT solvers rely on a dynamic decision literal heuristic. They periodically restart the proof search to apply the effects of a changed heuristic. This helps the calculus focus on a part of the initial clauses where it can make progress. Upon a restart, some learned clauses may be removed, and the trail is reset to  . Since our calculus has a rule, the rule needs only to clear the trail. Adding to yields . However, this calculus does not terminate, because can be applied infinitely often.

A working strategy is to gradually increase the number of transitions between successive restarts. This is formalized via a locale parameterized by a base calculus and an unbounded function  . Nieuwenhuis et al. require f to be strictly increasing, but unboundedness is sufficient.

The extended calculus operates on states of the form , where is a state in the base calculus and n counts the number of restarts. To simplify the presentation, we assume that bases states are pairs (M, N). The calculus starts in the state and consists of two rules:The symbol represents the base calculus transition relation, and denotes an m-step transition in . The in reminds us that we count the number of transitions; in Sect. 4.5, we will review an alternative strategy based on the number of conflicts or learned clauses. Termination relies on a measure \(\mu _V\) associated with that may not increase from restart to restart: If , then . The measure may depend on V,  the number of variables occurring in the problem.

We instantiated the locale parameter with and f with the Luby sequence (\(1, 1, 2, 1, 1, 2, 4, \cdots \)) [35], with the restriction that no clause containing duplicate literals is ever learned, thereby bounding the number of learnable clauses and hence the number of transitions taken by  .

Figure 1a summarizes the syntactic dependencies between the calculi reviewed in this section. An arrow indicates that is defined in terms of . Figure 1b presents the refinements between the calculi. An arrow indicates that we proved or some stronger result—either by locale embedding ( ) or by simulating ’s behavior in terms of .

Independently from the previous section, we formalized DPLL as described in . The calculus operates on states (M, N), where M is the trail and N is the initial clause set. It consists of three rules: performs chronological backtracking: It undoes the last decision and picks the opposite choice. Conclusive states for are defined as for (Sect. 3.3).

The termination and partial correctness proofs given by Weidenbach depart from Nieuwenhuis et al. We also formalized them:

Termination is proved by exhibiting a well-founded relation that includes . Let V be the number of distinct variables occurring in the clause set N. The weight \(\nu \,L\) of a literal L is 2 if L is a decision literal and 1 otherwise. The measure isLists are compared using the lexicographic order, which is well founded because there are finitely many literals and all lists have the same length. It is easy to check that the measure decreases with each transition:

The proof is analogous to the proof of Theorem 2. Some lemmas are shared between both proofs. Moreover, we can link Weidenbach’s DPLL calculus with the version we derived from in Sect. 3.3:

This provides another way to establish Theorems 6 and 7. Conversely, the simple measure that appears in the above termination proof can also be used to establish the termination of the more general calculus (Theorem 1).

The calculus operates on states , where M is the trail; N and U are the sets of initial and learned clauses, respectively; and D is a conflict clause, or the distinguished clause \(\top \) if no conflict has been detected.

In the trail M,  each decision literal L is marked as such (\(L^\dag \)—i.e., ), and each propagated literal L is annotated with the clause C that caused its propagation (\(L^C\)—i.e., ). The level of a literal L in M is the number of decision literals to the right of the atom of L in M, or 0 if the atom is undefined. The level of a clause is the highest level of any of its literals, with 0 for \(\bot \), and the level of a state is the maximum level (i.e., the number of decision literals). The calculus assumes that N contains no clauses with duplicate literals and never produces clauses containing duplicates.

The calculus starts in a state . The following rules apply as long as no conflict has been detected:The and rules generalize their counterparts. Once a conflict clause has been detected and stored in the state, the following rules cooperate to reduce it and backtrack, exploring a first unique implication point [6, Chapter 3]:Exhaustive application of these three rule corresponds to a single step by the combined learning and nonchronological backjumping rule from . The rule is even more general and can be used to express learned clause minimization [54].

In , \(C \cup D\) is the same as \(C \vee D\) (i.e., \(C \uplus D\)), except that it keeps only one copy of the literals that belong to both C and D. When performing propagations and processing conflict clauses, the calculus relies on the invariant that clauses never contain duplicate literals. Several other structural invariants hold on all states reachable from an initial state, including the following: The clause annotating a propagated literal of the trail is a member of \(N \uplus U.\) Some of the invariants were not mentioned in the textbook (e.g., whenever \(L^C\) occurs in the trail, L is a literal of C). Formalization helped develop a better understanding of the data structure and clarify the book.

Like , has a notion of conclusive state. A state is conclusive if \(D = \top \) and \(M\vDash N\) or if \(D = \bot \) and N is unsatisfiable. The calculus always terminates, but without a suitable strategy, it can block in an inconclusive state. At the end of the following derivation, neither nor can process the conflict further:

To prove correctness, we assume a reasonable strategy: and are preferred over ; and are not applied. (We will lift the restriction on and in Sect. 4.5.) The resulting calculus, , refines with the assumption that derivations are produced by a reasonable strategy. This assumption is enough to ensure that the calculus can backjump after detecting a nontrivial conflict clause other than \(\bot \). The crucial invariant is the existence of a literal with the highest level in any conflict, so that can be applied. The textbook suggests preferring to and to the other rules. While this makes sense in an implementation, it is not needed for any of our metatheoretical results.

Once a conflict clause has been stored in the state, the clause is first reduced by a chain of and transitions. Then, there are two scenarios: (1) the conflict is solved by a , at which point the calculus may resume propagating and deciding literals; (2) the reduced conflict is \(\bot \), meaning that N is unsatisfiable—i.e., for unsatisfiable clause sets, the calculus generates a resolution refutation.

The calculus is designed to have respectable complexity bounds. One of the reasons for this is that the same clause cannot be learned twice:

The formalization of this theorem posed some challenges. The informal proof in is as follows (with slightly adapted notations):

Proof  By contradiction. Assume CDCL learns the same clause twice, i.e., it reaches a state where is applicable and More precisely, the state has the form where the \(K_i\), \(i>1\) are propagated literals that do not occur complemented in D, as otherwise D cannot be of level i. Furthermore, one of the \(K_i\) is the complement of L. But now, because is false in and instead of deciding the literal L should be propagated by a reasonable strategy. A contradiction. Note that none of the \(K_i\) can be annotated with . \(\square \)

Many details are missing. To find the contradiction, we must show that there exists a state in the derivation with the trail \(M_2K^\dag M_1\), and such that \(D\vee L \in N \uplus U.\) The textbook does not explain why such a state is guaranteed to exist. Moreover, inductive reasoning is hidden under the ellipsis notation (\(K_n\cdots K_2\)). Such a high-level proof might be suitable for humans, but the details are needed in Isabelle, and Sledgehammer alone cannot fill in such large gaps, especially if induction is needed. The first version of the formal proof was over 700 lines long and is among the most difficult proofs we carried out.

We later refactored the proof. Following the book, each transition in was normalized by applying and exhaustively. For example, we defined so that if and cannot be applied to and for some state T. However, normalization is not necessary. It is simpler to define as , with the same condition on as before. This change shortened the proof by about 200 lines. In a subsequent refactoring, we further departed from the book: We proved the invariant that all propagations have been performed before deciding a new literal. The core argument (“the literal L should be propagated by a reasonable strategy”) remains the same, but we do not have to reason about past transitions to argue about the existence of an earlier state. The invariant also makes it possible to generalize the statement of Theorem 10: We can start from any state that satisfies the invariant, not only from an initial state. The final version of the proof is 250 lines long.

Using Theorem 10 and assuming that only backjumping has a cost, we get a complexity of \(\mathrm {O}(3^V)\), where V is the number of different propositional variables. If is always preferred over , the learned clause is never redundant in the sense of ordered resolution [57], yielding a complexity bound of \(\mathrm {O}(2^V)\). We have not formalized this yet.

In , and in our formalization, Theorem 10 is also used to establish the termination of . However, the argument for the termination of also applies to irrespective of the strategy, a stronger result. To lift this result, we must show that refines .

It is interesting to show that refines , to establish beyond doubt that is a CDCL calculus and to lift the termination proof and any other general results about . The states are easy to connect: We interpret a tuple as a pair , ignoring C.

The main difficulty is to relate the low-level conflict-related rules to their high-level counterparts. Our solution is to introduce an intermediate calculus, called , that combines consecutive low-level transitions into a single transition. This calculus refines both and and is sufficiently similar to so that we can transfer termination and other properties from to through it.

Whenever the calculus performs a low-level sequence of transitions of the form , the calculus performs a single transition of a new rule that subsumes all four low-level rules:When simulating in terms of , two interesting scenarios arise. First, ’s behavior may comprise a backjump: The rule can be simulated using ’s rule. The second scenario arises when the conflict clause is reduced to \(\bot \), leading to a conclusive final state. Then, has no counterpart in . The two calculi are related as follows: If , either or is a conclusive state. Since is well founded, so is . This implies that without terminates.

Since is mostly a rephrasing of , it makes sense to restrict it to a reasonable strategy that prefers and over , yielding . The two strategy-restricted calculi have the same end-to-end behavior:

We could use the same strategy for restarts as in Sect. 3.5, but we prefer to exploit Theorem 10, which asserts that no relearning is possible. Since only finitely many different duplicate-free clauses can ever be learned, it is sufficient to increase the number of learned clauses between two restarts to ensure termination. This criterion is the norm in modern SAT solvers. The lower bound on the number of learned clauses is given by an unbounded function . In addition, we allow an arbitrary subset of the learned clauses to be forgotten upon a restart but otherwise forbid . The calculus that realizes these ideas is defined by the two rulesWe formally proved that is totally correct. Figure 2 summarizes the situation, following the conventions of Fig. 1.

As a step towards formalizing SMT, we designed a calculus that provides incremental solving on top of :We first run the calculus on a clause set N, as usual. If N is satisfiable, we can add a nonempty, duplicate-free clause C to the set of clauses and apply one of the two above rules. These rules adjust the state and relaunch .

The key is to prove that the structural invariants that hold for still hold after adding the new clause to the state. Then the proof is easy because we can reuse the invariants we have already proved about .

The two-watched-literal (2WL or TWL) scheme [42] is a data structure that makes it possible to efficiently identify candidate clauses for unit propagation and conflict. In each non-unit clause, we distinguish two watched literals—the other literals are unwatched. Initially, any of a non-unit clause’s literals can be chosen to be watched. In the simplest version of the scheme, the solver maintains the following invariant for each non-unit clause:As a consequence of this invariant, setting an unwatched literal will never yield a candidate for propagation or conflict, because the two watched literals can then only be true or unset.

For each literal L, the clauses that contain a watched L are chained together in a list (typically a linked list). When a literal L becomes true, the solver needs only to iterate through the list associated with \(-L\) to find candidates for propagation or conflict. For each candidate clause, there are four possibilities:

In , a weaker invariant is used, inspired by MiniSat [18]:This invariant is easier to establish than (\(\alpha \)): If the other watched literal is true, there is nothing to do, regardless of the truth value of the unwatched literals. The four-step procedure above can easily be adapted, by pulling step 2.3 to the front.

To illustrate how the solver maintains the invariant, whether (\(\alpha \)) or (\(\beta \)), we consider the small problem shown in Fig. 3. The clauses are numbered from 1 to 4. Gray cells identify watched literals. Thus, clause 1 is \(\lnot \,B\vee C \vee A\), where \(\lnot \,B\) and C are watched.Upon backtracking, there is no need to update the data structure. A key property for the data structure’s efficiency is that the invariant is preserved when we remove literals from the trail.

In MiniSat and other implementations, propagation is performed immediately whenever a suitable clause is discovered, and when a conflict is detected, the solver stops updating the data structure and processes the conflict. Using this more efficient strategy, the following scenario is possible for the example of Fig. 3:By making the right arbitrary choices, we could go from propagation to propagation without having to update the clauses. However, neither invariant holds for clauses 1 to 3 after step 3. To capture the new state of affairs, we need a more precise invariant and a richer notion of state that take into account any pending updates. The new invariant is as follows:An update is represented by a pair (L, C), where L is a literal that has become false and C is a clause that has L as one of its watched literals. Each time a literal L is added to the trail, all possible updates \((-L,\, C)\) are added to the set of pending updates, which is initially empty. Whenever a conflict is detected, the updates are reset to \(\emptyset \). Pending updates can be processed at any time by the calculus.

CDCL with the 2WL data structure is defined as an abstract calculus that refines . Nonunit clauses are represented as , where is the multiset of watched literals (of cardinality 2) and the multiset of unwatched literals. Unit clauses are represented as singleton multisets. The state must also keep track of pending updates. States have the form , where and do not influence the calculus; they are ghost components that are useful for connecting a 2WL state to the format expected by :The function converts a 2WL clause set to a standard clause set.

The first two rules of have direct counterparts in :For both rules, the side condition is necessary because invariant (\(\beta \)) is not required to hold for C while a (L, C) update is pending.

The next rules manipulate the state’s 2WL-specific components, without affecting the state’s semantics as seen through :As in , propagations and conflicts are preferred over decisions. This is achieved by checking that and \( Q \) are empty when making a decision:The restriction on is enough to ensure that the reasonable strategy is applied in . and are as before, except that they also preserve the 2WL-specific components of the state. The rule is replaced by two rules, because of the distinction between unit and nonunit clauses:

refines in the following sense:

refines ’s end-to-end behavior and produces final states that are also final states for . We can apply Theorem 9 to establish partial correctness.

The next step is to refine the calculus with watched literals to an executable program. The state is a tuple , where is a list (instead of a set) of clauses containing first n initial nonunit clauses followed by the learned nonunit clauses, where clauses are represented as lists of literals starting with the watched ones; M uses indices in to represent clause annotations; and uses indices in to represent clauses. The D, , , and Q components are as before.

The program’s main loop invokes functions that implement specific rules or set of rules. The function for , , , and is presented below:

The values , , and correspond to positive, negative, and undefined polarity, respectively. As we refine the program, we must provide additional invariants for the data structure—for example, indices in are valid and is a valid index. The assertion corresponding to the latter, , is not shown above, but it is needed for code generation.

The main loop is called . Although it imposes an order on rule applications, it is not fully deterministic—for example, it does not specify which literal to choose in . The following theorem connects it to the calculus:

The state returned by the program is final for , which means by Theorem 13 that it is also final for . We conclude that the program is a partially correct implementation of . In addition, since the specification always specifies a non- result, the program always terminates normally.

In a further refinement step not presented here, we extend the state with watch lists that map from a literal to the clauses that are watched, instead of recalculating them each time. The watch lists are modeled by a function such that and update it in when required.

To be complete in a practical sense, an executable SAT solver must first initialize the 2WL data structure, run the calculus, and return “satisfiable” (with a model) or “unsatisfiable,” depending on whether a conflict has been found. The initialization step is necessary not only to run the program on actual problems but also to ensure that it is possible to create a 2WL state that satisfies invariant (\(\gamma \)) for any input.

The input is a list of clauses, where each clause is itself a list. We require that the lists are nonempty and contain no duplicates. For each clause C, we perform the following steps:The result is a well-formed state that satisfies invariant (\(\gamma \)). If a conflict is found in step 1.2, the program can answer “unsatisfiable” immediately.

Before we can generate imperative code, we must first eliminate the remaining nondeterminism, notably the choice of literal in . We implement the variable-move-to-front heuristic [5]. During initialization, we create a list containing all the literals. This list is used to initialize the doubly linked list needed by the heuristic. We also extract the maximal atom in the list to allocate the list of the polarity-checking optimization (Sect. 6.5) with the correct length.

Second, we must specify the data structures to use the generated code. Lists of clauses are refined to resizable arrays of nonresizable arrays. The dynamic aspect is required for adding learned clauses. Within a clause, only the order of literals needs to change. We had to formalize the data structure ourselves; for technical reasons, the resizable arrays from the Imperative Collection Framework [29, 31] cannot contain arrays. We were able to reuse some of the theorems proved on the separation logic level.

We used Sepref to refine the code of the SAT solver, including initialization. We restrict the type of the atoms to natural numbers . In our first version, we also used (unbounded) natural number to literals in the generated code: The literals and are encoded by the numbers \(2\cdot i\) and \(2\cdot i +1\), respectively. However, the extraction of an atom from the literals (the integer division by 2) was inefficient in Standard ML. Therefore, we changed our representation to 32-bits unsigned integers (so only \(2^{31}\) atoms are allowed). The extraction of atoms now becomes bit-shifting.

The end-to-end refinement theorem, relating a semantic satisfiability check on the input problem ( that returns if unsatisfiable) to the Imperative HOL heap code ( ), is stated below, where the relation refines a multiset of multisets of literals to a list of lists of 32-bit unsigned integers, and the relation refines the model that is returned as a list of literals.

Using stepwise refinement, we integrate this optimization into the imperative data structure used for the trail. This refinement step is isolated from the rest of the development, which only relies on its final result: a more efficient implementation of the trail and its operations. As Lammich observed elsewhere [32], this kind of modularity is invaluable when designing complex data structures.

Since the atoms are natural numbers, we enrich the trail data structure with a list of polarities (of type ), such that the \((i + 1)\)st element gives the polarity of atom i. The new function is defined as follows:

Given \(N_1\) the set of all valid literals (i.e., the positive and negative version of all atoms that appear in the problem), the refinement relation between the trail with the list of polarities and the simple trail is defined as follows:

This invariant ensures that the list is long enough and contains the polarities. We can link the new polarity function to the simpler one. If , then

In a subsequent refinement step, we use Sepref to implement the list of polarities by an array, and atoms are mapped to 32-bits unsigned integers ( ), as in Sect. 6.4. Accordingly, we define two auxiliary relations:Sepref generates the imperative program and derives the following refinement theorem:

The precondition, in square brackets, ensures that we can only take the polarity of a literal that is within bounds. The term after the arrow is the refinement for the result, which is trivial here because the data structure for polarities remains .

Composing the refinement steps (1) and (2) yields the theorem

where combines the two refinement relations for trails and . The precondition is a consequence of \(L \in N_1\) and the invariant . If we invoke Sepref now and discharge ’s preconditions, all occurrences of the unoptimized function are be replaced by . After adapting the initialization to allocate the array for of the correct size, we can prove end-to-end correctness as before with respect to the optimized code (cf. Theorem 15).