1 Introduction↩︎

The Satisfiability (SAT) problem asks whether a Boolean formula admits an assignment of truth values to its variables that makes the formula true. Despite this simple formulation, SAT is a central problem in both theoretical computer science and practical computing. It was the first problem shown to be NP-complete [1], and its generality makes it a natural target for encoding a wide range of combinatorial problems. As a result, improvements in SAT solving can often be translated into improvements for many other computational tasks.

SAT solvers are algorithms designed to decide this problem. Through sophisticated heuristics and search algorithms, they navigate enormous search spaces and make even very large SAT instances tractable [2]. Beyond optimization and planning tasks, SAT solvers have become critical tools for verifying large mathematical proofs that are infeasible to check by hand, such as the Boolean Pythagorean Triples problem [3] resulting in a 200-terabyte proof. Another example is Schur Number Five [4], producing a proof of roughly 2 petabytes.

These applications make it important to ensure the correctness of SAT solvers themselves since even small bugs could compromise the validity of the results they produce [5]. Interactive theorem provers (ITPs), such as Rocq [6] or Isabelle [7], provide a way to formally verify such systems and obtain strong guarantees about their behavior. In Rocq, definitions, theorem statements, and proofs are written in a formal language, and completed proofs are checked by a small trusted kernel. This means that the results established in this paper are justified not only by informal mathematical argument, but also by machine-checked proof terms.

The central objective of this paper is to formalize and verify, in Rocq, the abstract transition-system presentation of SAT solving introduced by Nieuwenhuis et al. [8]. This presentation captures the Davis–Putnam–Logemann–Loveland (DPLL) procedure not as an executable algorithm, but as a collection of transitions between solver states. One contribution of this paper is to formalize these transition rules in Rocq and establish their key metatheoretic properties, namely correctness, completeness, and termination. This objective is motivated by two considerations. First, the transition-system view gives a compact and transparent account of SAT solving, which makes it particularly suitable for formal reasoning. Second, it provides a natural starting point for later extensions toward more expressive frameworks such as DPLL(T), and therefore a useful basis for future verification efforts.

Closely related work has already been carried out in Isabelle/HOL. In particular, Blanchette et al. [9] formalize abstract DPLL and CDCL calculi based on Nieuwenhuis et al.and refine them toward executable solvers. Compared to that work, we contribute an abstract notion of strategy for SAT solving, and instantiate this framework with a concrete strategy that is subsequently extracted to OCaml.

From this perspective, the aim of the paper is not to verify a highly optimized modern SAT solver directly, but rather to verify the correctness of an abstract model of SAT solving from which concrete solving procedures can later be derived. In doing so, the paper connects the abstract theory of DPLL with a machine-checked formalization in Rocq, and thereby provides a small but trustworthy verified core on which further extensions can build. Throughout the paper, references to formal objects are presented using hyperlink macros that allow the reader to move directly from the informal exposition to the corresponding definition, lemma, or theorem in the generated Rocq documentation.

The paper is organized as follows. Section 2 presents the necessary background on propositional logic and satisfiability. Section 3 then introduces the transition system of Nieuwenhuis et al. [8] and its formalization, including proofs of correctness, completeness, and termination. Building on this, Section 4 shows how solving procedures can be derived from the transition system using strategies and presents a concrete implementation of such a strategy. Finally, Section 5 discusses the scope, limitations, and future directions of the formalization.

Summarizing the contributions of this work, we

• prove an if-and-only-if characterization of satisfiability. Compared to Nieuwenhuis et al. [8], we not only show that derivations to a final non-fail state give a model, but also that, conversely, every satisfiable formula gives rise to such a derivation. For that converse direction we introduce a new normalization procedure.

• include the pure literal rule in our transition system. This rule is part of the original DPLL procedure, but Nieuwenhuis et al. [8] leave it out of their transition system. To add this rule, we strengthen the entailment development, see 21 7.

• introduce an abstract notion of strategy, which lets one derive verified solvers from the transition system. We also give one concrete implementation of such a strategy, and extract and test it on a collection of SAT benchmarks.

• formalize the whole development in Rocq.

For reproducibility, the full Rocq formalization is publicly available in the RocqSAT repository¹, and HTML documentation is available on GitHub Pages². The formalization depends on Rocq 9.0. In its current form, the development contains 187 lemmas, 7 theorems, 75 definitions, and 14 examples. Of these 75 definitions, 30 are standard Rocq definitions, 36 are Equations definitions, and 9 are inductive Rocq definitions. Altogether, the formalization consists of 3555 lines of code, of which 2403 lines are proof scripts between Proof. and Qed. Throughout the paper, definitions and results are accompanied by a link to the HTML documentation of the corresponding Rocq identifier (e.g., ).

The repository also contains the extracted solver for Ocaml and several sample SAT problems on which to try the solver.

2 Propositional Logic↩︎

We begin by recalling the standard definition of satisfiability for propositional formulas. The notions introduced in this section are classical and can be found in standard textbooks on logic and formal reasoning, such as Huth and Ryan’s Logic in Computer Science [10]. We first introduce the basic syntactic elements used to construct propositional formulas.

For the following definitions we fix a finite set of propositional symbols \(P\).

A literal corresponds to either a positive or a negative occurrence of an atom, enabling formulas to represent both assertions and their negations.

Literals can then be combined into clauses.

Formulas are often expressed in conjunctive normal form. This form is convenient for reasoning about satisfiability and is the standard input for many SAT-solvers. Although this may appear to be a restriction, it does not lose generality, since every propositional formula can be transformed into an equivalent formula in conjunctive normal form.

While this set-based definition of partial assignments is natural, it is cumbersome for formal verification. We instead represent partial assignments as lists. This choice is motivated by the fact that the list type supports well-behaved induction principles, which facilitate formal reasoning, and also allows a partial assignment to be interpreted as a trace of assignments.

Each literal is also annotated with a type Ann . We add the superscript \(d\) to a literal, writing \(l^d\), to indicate that it is a decision literal. These annotations will be ignored during evaluation, but are essential for defining and reasoning about the DPLL transition rules.

To recover set-like behavior, we require an additional property.

Let \(m\) be a partial assignment. We define a three-valued evaluation function \[[\![\cdot]\!]_{m} : \texttt{Lit} + \texttt{Clause} + \texttt{CNF} \;\to\; \{\texttt{T}, \texttt{F}, \texttt{U}\}.\] In a slight abuse of notation, we write \(l \in m\) to mean that \(l\) appears in \(m\) before any occurrence of \(\neg l\), evaluating the list from head to tail. Note that this notation coincides with its standard definition for well-formed partial assignments.

One benefit of the list-based representation is that evaluation is defined for arbitrary lists of literals, not only for well-formed partial assignments. This lets us reason about more general lists throughout the formalization, while only introducing well-formedness assumptions in the lemmas that require them. By contrast, in a set-based approach, a set containing both \(x\) and \(\neg x\) cannot be evaluated without imposing an additional well-formedness condition.

3 Transition Systems↩︎

We now introduce the transition system framework used to describe the DPLL procedure.

Having defined states, we now formalize how one state can evolve into another.

To model the DPLL procedure, we consider a collection of transition rules. In the following definitions, let \(T\) denote such a set of transition rules.

To state later lemmas and theorems, we consider sequences of transitions, motivating the reflexive–transitive and transitive closures of the transition system.

Finally, to reason about termination, we introduce the notion of a final state.

3.1 Transition System for DPLL↩︎

We now specialize the general transition-system framework to the DPLL procedure. Following Nieuwenhuis et al. [8], we describe DPLL as a set of transition rules on states. We first give an informal overview of this transition-system view, before defining the rules formally.

In this formulation, the solver gradually extends a partial assignment until it either finds a satisfying assignment or reaches a conflict, applying any rule whose conditions are satisfied. The UnitPropagate rule applies when a clause has become unit, meaning that all but one of its literals have been assigned false, so the remaining literal must be assigned true to satisfy the clause. The Pure rule assigns a pure literal, that is, a literal whose negation does not occur in the formula, since doing so cannot create a conflict. The Decide rule makes a branching choice by assigning a previously undefined literal as a decision literal. If a conflict is reached, then Backtrack returns to an earlier decision point, undoes later assignments, and flips that decision, with the flipped literal no longer marked as a decision literal. If no earlier decision remains to be undone, Fail applies, indicating that the formula is unsatisfiable.

This is formalized by the following transition rules:

\[\begin{align} \textrm{UnitPropagate:}\quad & m \parallel f \land (c \lor l) \;&\Longrightarrow&\quad m\, l \parallel f \land (c \lor l) & \text{if } & \begin{cases} c \text{ is false in } m \\ l \text{ is undefined in } m \end{cases} \\ \textrm{Decide:}\quad & m \parallel f \;&\Longrightarrow&\quad m\, l^{d} \parallel f & \text{if } & \begin{cases} l \text{ or } \neg l \text{ occurs in a clause of } f \\ l \text{ is undefined in } m \end{cases} \\ \textrm{Fail:}\quad & m \parallel f \land c \;&\Longrightarrow&\quad \texttt{fail} & \text{if } & \begin{cases} c \text{ is false in } m \\ m \text{ contains no decision literals} \end{cases} \\ \textrm{Backtrack:}\quad & m\, l^{d}\, n \parallel f \land c\;&\Longrightarrow&\quad m\, \neg l \parallel f \land c & \text{if } & \begin{cases} c \text{ is false in } m\, l^{d}\, n \\ n \text{ contains no decision literals} \end{cases} \\ \textrm{Pure:}\quad & m \parallel f \;&\Longrightarrow&\quad m\, l \parallel f & \text{if } & \begin{cases} l \text{ occurs in a clause of } f \\ \neg l \text{ occurs in no clause of } f \\ l \text{ is undefined in } m \end{cases} \end{align}\]

We now distinguish between two transition systems. We refer to the transition system containing all of the rules above as the classical DPLL system. We also define the base DPLL system as the subsystem containing only Decide, Fail, and Backtrack. We will later show that this smaller system is still sufficient for defining a complete solving procedure.

We now provide some examples of how this transition system can be applied.

3.2 Correctness↩︎

We show that the classical DPLL transition system is sound and complete with respect to satisfiability. In particular, we prove that the existence of a derivation from the initial state to a final state precisely characterizes whether a formula is satisfiable or unsatisfiable.

We first show that every final state encodes a model of the formula.

Next, we show that if there exists a partial assignment \(m\) satisfying \(f\), then there exists a partial assignment \(m'\) such that there is a derivation from the initial state \(\emptyset \parallel f\) to a final state \(m' \parallel f\). To establish this, we use a process called normalization ](https://vlamonster.github.io/RocqSAT/RocqSAT.Normalization.html#normalize). This process has four steps. First, we totalize [ the partial assignment, so that every literal occurring in \(f\) is defined. Next, we convert propagation annotations ](https://vlamonster.github.io/RocqSAT/RocqSAT.Normalization.html#convert_prop) to decision annotations. We then bound [ the partial assignment by \(f\), removing any literals whose atoms do not occur in \(f\). Finally, we deduplicate the partial assignment, making it duplicate-free.

To show that the normalized state can be reached from the initial state and is final, we first establish the invariants of this normalization procedure. Each step establishes a new invariant that is preserved by all later steps, which gives rise to a number of intermediate lemmas. For brevity, we only state the results for the complete normalization procedure.

First, normalization preserves the property of being a model of \(f\).

After totalization, every literal occurring in \(f\) is defined.

After converting all annotations, every literal is a decision literal.

After bounding, the partial assignment is bounded by \(f\).

Finally, after deduplication, the partial assignment is duplicate-free.

It remains to show that a derivation to the normalized state exists. For this, we first prove an auxiliary lemma showing that every well-formed partial assignment consisting only of decision literals can be reached from the initial state \(\emptyset \parallel f\).

We obtain the desired result by specializing this lemma to the normalized partial assignment.

We now show that satisfiability is reflected in the existence of a derivation to a final state. The forward direction follows directly from 1. The converse direction, however, does not appear in this form in Nieuwenhuis et al. [8], and is proved here using the normalization procedure introduced above.

There is an analogous theorem for unsatisfiability, but before stating and proving it, we first introduce the notions of model-preserving literals and locally model-preserving literals, which we will need in order to define entailment.

We can now define entailment. Intuitively, this property expresses that propagated literals appearing in the tails of partial assignments derived by the transition rules are logical consequences of the literals that precede them.

This definition is loosely based on the one given by Nieuwenhuis et al. [8], with the addition of the third case involving model-preserving literals. This extra case is needed to account for the Pure rule in our transition system. One could go a step further and strengthen the classical Pure rule by considering a literal pure whenever it appears with only one polarity among the clauses that remain undefined under a given partial assignment. In that setting, the third case would need to use locally model-preserving literals instead.

We now wish to relate entailment to unsatisfiability. For this, we show two things. Firstly, entailment is preserved by the transition system. Secondly, for partial assignments containing no decision literals, entailment coincides with logical entailment. We show the second first.

The next lemma shows that entailment is preserved under the transition system. Since a full formal proof depends on a number of technical lemmas, we only give some intuition for the argument here. The proof proceeds by case analysis on the applied transition rule. For Fail, the assumptions lead directly to a contradiction. For Decide and Pure, the second and third cases of the entailment definition apply directly. The argument for the Backtrack and UnitPropagate rules is more subtle, since they require unpacking how the original entailment was constructed. The key idea is that repeatedly unpacking this construction must eventually lead either to a contradiction or to a point where one of the entailment cases applies.

It follows immediately that the same holds not only for transitions, but also for derivations.

Before the main result, we first state one final lemma about derivations to fail.

We now have all the tools needed to show how unsatisfiability is characterized by the fail state. The reverse direction relies on a result we will show in the next subsection. This theorem corresponds closely to part (1) of Theorem 2.12 in Nieuwenhuis et al. [8].

3.3 Termination↩︎

To show termination of any procedure based on the transition system introduced above, we use the standard notions of accessibility and well-foundedness. Intuitively, an element is accessible if all elements below it are themselves accessible, where the notion of below is determined by the relation under consideration. A relation is well-founded if every element is accessible, that is, if accessibility can always be established by a finite proof. This provides a convenient way to prove termination, since once the transition relation is shown to be well-founded, every sequence of transitions must eventually terminate. In the Rocq standard library, these notions are represented by the propositions Acc and well_founded.

Inductive Acc (x : A) : Prop :=
| Acc_intro : (forall y : A, R y x -> Acc y) -> Acc x.

Definition well_founded := forall a : A, Acc a.

For the termination arguments below, we use several standard definitions and lemmas concerning relations from the standard library, including definitions of inclusion of relations, closure operations on relations, and commutation of relations.

We now introduce a well-founded relation on bounded lists of natural numbers that will be used in the termination argument.

Note that this is not quite the standard lexicographic order on lists. In the standard lexicographic order, a list can be smaller simply because it is shorter. By contrast, \(\texttt{PrefixLt}_t\) only compares lists at the first position where they differ.

It follows from the well-foundedness of \(<\) on the natural numbers that this relation is well-founded for every choice of \(t\).

We now formalize the termination argument used by Nieuwenhuis et al.to show that the classical DPLL system is well-founded. The idea is to equip states with two measures, score and score_total, and to show that every transition rule decreases with respect to one of them. More precisely, we will prove that all transition rules except Fail decrease with respect to the lexicographic product of these measures, together with the prefix order and the standard order \(<\) on the natural numbers.

We briefly illustrate these measures on the transition rules from Example 3. For convenience, we write TotalLt [](https://vlamonster.github.io/RocqSAT/RocqSAT.Termination.html#TotalLt) for the standard order \(<\) on the natural numbers. The key point is that along each transition, the measure score decreases with respect to PrefixLt, and if score remains unchanged, then score_total decreases with respect to TotalLt.

To complete the termination argument, it remains to account for the state fail. For this purpose, we introduce the relation FailLt [](https://vlamonster.github.io/RocqSAT/RocqSAT.Termination.html#FailLt), which holds exactly when the left-hand side is fail and the right-hand side is a non-fail state. In this way, fail becomes smaller than every non-fail state, which leads to the following relation on states.

It follows that this relation is well-founded.

Finally, we show that \(\Longrightarrow\) is well-founded. The key observation is that, for every state, there exists a formula \(f\) such that the transition relation is included in \(\ll_f\). The claim then follows, using the well-foundedness of \(\ll_f\) established above.

4 Solve Procedures↩︎

The transition system from the previous section provides an abstract description of DPLL and establishes its key properties, in particular correctness, completeness, and termination. We now show how to turn this abstract system into a solving procedure. The main idea is to equip the transition system with a strategy that determines, for each non-final state, which transition to take next. We then obtain a solver based on such a strategy by repeatedly applying it until a final state is reached.

4.1 Abstract Solve Procedure↩︎

We formalize this by introducing strategies as functions from states to optional successor states, where None indicates a final state, and that satisfy the following conditions.

We highlight two aspects of this definition that will be important in what follows.

First, we require only that a strategy step follows a strict derivation, rather than a single transition. This allows a strategy to combine several transition steps into one, for example by making multiple decisions at once. Although efficiency is not the main focus of this paper, this flexibility is still useful, since it allows the abstract notion of strategy to cover a broader range of solving procedures.

Second, the requirement that next returns None only on states that are final in \(B\) is sufficient because the rules in \(B\) already capture the essential search structure of DPLL. The additional rules UnitPropagate and Pure do not lead to fundamentally new search states. Rather, they only allow certain literals to be assigned by propagation instead of by explicit decision, which can speed up the search. Thus, being final in \(B\) is equivalent to being final in \(C\), as stated in the following lemma.

Given a strategy next, we define the induced solver by iterating next from the initial state until a final state is reached. This solver is well-defined, since its iteration must terminate. Each application of next yields a step in the transitive closure \(\Longrightarrow^+\) of the transition relation. Because \(\Longrightarrow\) is well-founded by Theorem 4, \(\Longrightarrow^+\) is well-founded as well. Hence the iteration of next cannot produce an infinite sequence of states.

By Lemma 13, any state returned by solve is final. It therefore follows from Theorems 1 and 3 that the solver behaves as expected. If solve returns fail, then the formula \(f\) is unsatisfiable, while if it returns a non-fail state of the form \(m \parallel f\), then \(m\) is a model of \(f\).

4.2 Concrete Solve Procedure↩︎

We now instantiate the abstract notion of strategy by defining a concrete function next_state. This function covers all transition rules of the classical DPLL system except for Pure. It first checks whether the current state contains a conflict. If so, it determines whether there is a decision literal to backtrack to. If there is none, it applies Fail. Otherwise, it applies Backtrack. If no conflict is present, it tries to find a unit clause, and if one is found, it applies UnitPropagate. Only if no conflict and no unit clause are found does it apply Decide. In this way, next_state yields a deterministic instance of the abstract strategy introduced above.

[lst:next_state] gives a simplified overview of this function, with the proof objects witnessing well-formedness omitted for readability. Here, ++p denotes concatenation with a propagated literal, and ++d denotes concatenation with a decision literal.

[
  language=Coq,
  caption={The concrete strategy \texttt{next\_state} \coqident{Strategy}{next_state}},
  label={lst:next_state},
  literate={¬}{{$\neg$}}1
]
Equations next_state (s: State): option State :=
next_state fail        := None;
next_state (state m f) :=
  match find_conflict m f with
  | Some c =>
    match split_last_decision m with
    | None         => Some fail
    | Some (m', l) => Some (state (m' ++p ¬l) f)
    end
  | _ =>
    match find_unit m f with
    | Some (c, l) => Some (state (m ++p l) f)
    | None        =>
      match find_decision m f with
      | Some l => Some (state (m ++d l) f)
      | None   => None
      end
    end
  end.

It remains to show that next_state is indeed a strategy. For this, we verify two properties. First, next_state is sound with respect to \(\Longrightarrow\), meaning that whenever it returns a successor state, that successor is obtained by a single transition step, and hence by a strict derivation. Second, next_state is complete with respect to \(\Longrightarrow_B\), meaning that whenever a transition in the base DPLL system is possible, next_state returns some successor state. Together with the fact that \(\texttt{next\_state}\;\texttt{fail} = \texttt{None}\), this is enough to conclude that next_state satisfies the definition of a strategy. These two properties are stated in the following lemmas.

4.3 Extraction to OCaml↩︎

In addition to the formalization of the transition system and solving procedures, the concrete solver was also extracted to OCaml using Rocq’s extraction mechanism. For this purpose, the basic datatypes bool, list, and nat were mapped to their OCaml counterparts using the extraction directives shown in [lst:extraction_ocaml].

Extract Inductive bool => "bool" [ "true" "false" ].
Extract Inductive list => "list" [ "[]" "(::)" ].
Extract Inductive nat => "int"
[ "0" "(fun x -> x + 1)" ]
"(fun zero succ n -> if n=0 then zero () else succ (n-1))".

The extracted solver, together with a small runner and instructions for how to execute it, is available in the repository.

To validate the extracted solver, we tested it on a number of simple SAT instances, many of them taken from Gregory Duck’s collection of SAT examples [11]. For all instances on which the solver finished, it produced the correct result. The largest example it was able to handle was zebra.cnf, which has 155 variables and 1135 clauses. Of course, the size of a SAT instance does not necessarily correspond directly to its difficulty, so this number should only be taken as a rough indication. The current extracted solver does not scale well to larger instances. The main expected reason is the choice of data structures in the formalization and in the concrete strategy. Currently, many operations require traversing lists, which leads to linear-time access. A more efficient implementation would use data structures supporting constant-time lookup, such as arrays or similarly indexed data structures. This would likely improve the practical performance substantially.

5 Discussion↩︎

In this paper, we formalized the DPLL transition system of Nieuwenhuis et al. [8] in Rocq. The formalization covers the core correctness, completeness, and termination results for DPLL, and extends the original development by also formalizing the pure literal rule. Together, these results show that the transition-system presentation of DPLL can be mechanized in an interactive theorem prover while preserving the intended semantic guarantees of the abstract solver.

At the same time, the results of this paper should be understood as an abstract verified core for SAT solving. The formalization establishes correctness, completeness, and termination for the DPLL transition system, and derives both an abstract solver and a concrete strategy from it. This gives strong guarantees about the logical correctness of the procedure, but it does not yet amount to a verification of the behavior of modern industrial SAT solvers. In particular, the paper focuses on an abstract transition-system presentation and on a simple verified strategy, rather than on the highly optimized algorithms and data structures used in practice.

A first limitation is therefore the scope of the transition system itself. The formalization covers classical DPLL together with the pure literal rule, but it does not yet include extensions that are central to modern SAT solving, such as non-chronological backtracking, clause learning, clause forgetting, and restarts [9], [12]. These mechanisms are precisely what make modern CDCL-based solvers effective on large benchmark instances. As in Blanchette et al. [9], learn and backjump are best treated together, since combining them ensures that the solver continues to make progress after new clauses are learned. Relatedly, this paper does not yet cover the second part of Nieuwenhuis et al. [8], namely the extension from SAT to DPLL(T). The current formalization can therefore be seen as addressing the propositional core of their work, while leaving the SMT-oriented generalization for future work.

A second limitation concerns the concrete strategy derived from the transition system. Although it is formally verified as a strategy, it is intentionally simple and is not designed for performance. In particular, the function next_state does not implement the Pure rule. More generally, no serious experimental evaluation of the extracted solver has been carried out beyond testing correctness on small SAT instances. Thus, the current solver should be understood as a verified proof of concept rather than as a practically competitive SAT solver. Future work could improve this strategy by incorporating techniques used in practical SAT solvers, such as the two-watched-literal scheme for efficient unit propagation and the VSIDS branching heuristic for choosing decision literals [13].

There are also limitations in the structure of the formalization itself. Currently, transition systems are treated as large relations rather than as modular collections of transition rules. This is sufficient for the results proved here, but it tends to produce large proofs that proceed by repeated case analysis over all rules at once. A more modular organization, for example in the style used by Marić [12], could make the formalization easier to extend and maintain by splitting larger arguments into smaller lemmas for individual rules.

Finally, several natural extensions remain open. One possibility is to enrich the transition system with additional rules that bring it closer to modern SAT solvers, in particular backjumping, learning, forgetting, and restarts. Another possibility is to use the present formalization as a basis for a verified SMT solver, since the framework of Nieuwenhuis et al. [8] is designed to generalize from SAT to DPLL(T). More abstract notions of solving procedure could also be considered, for example by letting strategies operate on states together with auxiliary context, allowing preprocessing steps and more efficient bookkeeping while still fitting into the same general framework.

References↩︎