QCP · Research

Verifying a CDCL solver in one week of collaboration

Working with GPT 5.6 sol and Opus 4.8, the QCP team established Rocq-checkable functional correctness proofs for a C-language SAT solver.

Read the code Read the proofs

SAT, or Boolean satisfiability, asks whether there is an assignment of values to Boolean variables that makes a formula true. A SAT solver answers this question. It may report SAT, meaning that it has found a satisfying assignment; UNSAT, meaning that no such assignment exists; or UNKNOWN, meaning that it has not reached a conclusion because of time or resource limits.

How can we check that the solver's answer is correct? For SAT, we can substitute the returned assignment into the formula and check every constraint. UNSAT is harder: failing to find a solution does not mean that no solution exists. Some modern SAT solvers therefore produce an unsatisfiability proof when they report UNSAT, allowing an independent checker to verify that particular result.

Can we instead prove the solver's algorithm and implementation correct, so that correctness does not depend on producing and checking a separate proof for each run? The desired guarantee is that, for a formula satisfying the input conditions, any SAT or UNSAT answer the solver returns is correct.

Working toward this goal, the QCP team collaborated with GPT 5.6 sol and Opus 4.8 to complete the functional correctness verification of a C-language CDCL SAT solver in one week. Using QCP and Rocq, the team established machine-checkable proofs for this implementation: when the input meets the specification, a SAT answer comes with an assignment satisfying the original formula, while an UNSAT answer means that the original formula has no satisfying assignment.

The code, annotations, and proofs are included in QCP 2.1.0. The work also documents a human–AI collaboration in program verification, turning correctness requirements for a single implementation into checkable proofs.

The CDCL algorithm

CDCL, short for Conflict-Driven Clause Learning, is a classic SAT-solving algorithm and the basis of many modern SAT solvers. As it searches for a variable assignment, it analyzes conflicts and learns new clauses to avoid revisiting search branches that have already been ruled out.

CDCL usually operates on formulas in conjunctive normal form (CNF). A CNF formula is a conjunction of clauses, each of which is a disjunction of literals. A literal is a Boolean variable or its negation. A formula with m clauses can be written as:

F = C_{1} \land \dots \land C_{m}, C_{i} = ℓ_{i 1} \lor \dots \lor ℓ_{i k_{i}}

For the formula to be true, at least one literal in every clause must be true. Starting with no variables assigned, the solver alternates between decisions and unit propagation. A decision selects an unassigned variable and tries a truth value. Unit propagation handles a clause whose only unassigned literal is accompanied by literals already known to be false. The remaining literal must be true for the clause to hold, so its value follows directly. Propagation repeats until no such clause remains or all literals in a clause become false, producing a conflict.

Consider this formula:

F = (x \lor y) \land (x \lor \neg y)

If the solver decides that x is false, the first clause requires y to be true, while the second requires it to be false. This conflict shows that the current decision cannot be extended to a solution. CDCL analyzes the cause of the conflict and derives a learned clause from existing clauses. Here, resolving on y yields the unit clause x:

\frac{x \lor y x \lor \neg y}{x}

More generally, resolution derives a new clause from two clauses containing p and ¬p, respectively. In the following rule, A and B represent the disjunctions of the remaining literals:

\frac{A \lor p B \lor \neg p}{A \lor B}

Conflict analysis repeatedly applies this rule along the reasons for unit propagation. The learned clause is a logical consequence of the original formula, so adding it cannot exclude any solution of that formula. Writing L for the learned clause gives:

F ⊨ L, F \equiv (F \land L)

After learning a clause, the solver undoes some assignments, returns to an earlier decision level, and continues propagation using the learned clause. This is called backjumping: the learned clause determines the destination level, which may skip several decision levels rather than retreating one at a time. In the example above, the solver retracts the decision that x is false and uses the learned clause at decision level 0 to infer that x is true. Both original clauses then hold, regardless of the value of y.

The algorithm repeats decisions, propagation, conflict analysis, learning, and backjumping. It returns SAT when it finds an assignment satisfying every clause. A conflict at decision level 0 establishes UNSAT. For further background, see Marques-Silva, Lynce, and Malik's Conflict-Driven Clause Learning SAT Solvers.

What we verified

The verification covers a C implementation of CDCL, including decisions, unit propagation, conflict analysis, clause learning, and backjumping. Its main entry point, cdcl_solver, coordinates these operations and returns the result.

The specification of cdcl_solver states the implementation's overall correctness requirement: if the input conditions hold before a call, the corresponding output conditions must hold when the solver returns. Require describes the input formula and initial program state; Ensure describes the result and the state at return. Verification of the individual operations supports this entry-point contract.

The following excerpt shows the contract's main structure, omitting auxiliary parameters. The ellipses are for presentation only; the full contract appears at the end of this section.

int cdcl_solver(sat_data* s) /*@
  With (F : cnf) ...
  Require cnf_wf(n, F) && solver_input_core(s, F, ...)
  Ensure
    (exists J, __return == 1 && models(J, F) &&
      solver_sat_arm_core(s, F, ..., J)) ||
    (__return == 0 && cnf_unsat(n, F) &&
      solver_unsat_arm_core(s, F, ...)) ||
    (__return == -2 &&
      solver_capacity_exhausted_arm_core(s, F, ...))
*/

Input conditions

F is the logical variable representing the original input formula, and n is the number of variables. cnf_wf(n, F) requires variable identifiers to range from 0 to n - 1. solver_input_core connects this logical formula to the C data structures pointed to by s. It requires that:

The clause table correctly stores the original formula F, with no learned clauses initially. Every clause in the original formula is nonempty.
All variables are initially unassigned, and the assignment, reason, and decision-level arrays are in the states required by the specification.
Structures and arrays satisfy the memory requirements, and clause states and counts agree with their actual contents. The variable count satisfies 0 ≤ n < INT_MAX, and the existing clauses fit within the clause table's capacity.

These are preconditions that the caller must establish. The entry-point contract starts from an already constructed solver state. Input parsing and initial-state construction must establish these conditions before calling the solver.

Guarantees when SAT is returned

__return denotes the function's return value. The first branch states that, when the function returns 1, there is an assignment J for which models(J, F) holds: J satisfies every clause of the original formula.

J ⊨ F

solver_sat_arm_core(..., J) further requires that J match the assignment represented by the C program's assignment array at return. The guarantee is therefore both that a solution exists and that the assignment actually stored by the program is a solution. F always denotes the original formula from before the call. Even if the solver adds learned clauses, its final assignment must satisfy that original formula.

Guarantees when UNSAT is returned

The second branch states that, when the function returns 0, cnf_unsat(n, F) holds: no assignment to these n variables satisfies the original formula.

\neg \exists J, J ⊨ F

This conclusion rules out every possible assignment, not just those tried during the search. The proof must establish that reaching this return branch is sufficient to conclude that the original formula has no solution. The contract's guarantee does not require the user to check a separate UNSAT proof produced by that particular run.

Capacity exhaustion and the scope of the proof

The third branch corresponds to return value -2: the clause table has exhausted its capacity and cannot accept more learned clauses. The specification preserves a description of the data structures and their memory in this branch, but makes no SAT or UNSAT claim. This is the unresolved case described in the introduction and must not be interpreted as evidence of unsatisfiability.

Each output branch also describes the memory state at return. For example, the SAT branch preserves the storage relation for the formula and connects the assignment array to J. The UNSAT branch retains the relevant array memory but does not promise that it contains a satisfying assignment. The proof must therefore cover updates to the implementation's state; correctness of the abstract algorithm alone is insufficient.

The contract establishes partial functional correctness: if the precondition holds and the function returns, its result satisfies one of the three branches above. This work does not prove that the function always terminates, nor that it always reaches a SAT or UNSAT answer before exhausting the clause table's capacity.

Technical note: the full cdcl_solver contract

The following is the function contract in QCP 2.1.0, with the function body omitted. Require gives the input conditions. The three Ensure branches correspond to satisfiability, unsatisfiability, and clause-table capacity exhaustion.

int cdcl_solver(sat_data* s )/*@ With (F : cnf) original_count (snap : dense_snapshot)
      (ranks : Z -> option nat) values reasons levels states true_counts unassigned
      row_table n live cap
    Require cnf_wf(n, F) &&
    solver_input_core(s, F, original_count, snap, ranks,
      values, reasons, levels, states, true_counts, unassigned, row_table, n, live, cap)
    Ensure
      (exists J, __return == 1 &&
      models(J, F) &&
        solver_sat_arm_core(s, F, original_count, snap, ranks, values, reasons,
          levels, states, true_counts, unassigned, row_table, n, live, cap, J)) ||
      (__return == 0 &&
      cnf_unsat(n, F) &&
        solver_unsat_arm_core(s, F, original_count, snap, ranks, values, reasons,
          levels, states, true_counts, unassigned, row_table, n, live, cap)) ||
      (__return == -2 &&
      solver_capacity_exhausted_arm_core(s, F, original_count,
        snap, ranks, values, reasons, levels, states, true_counts, unassigned,
        row_table, n, live, cap))
*/

Definitions of the corresponding state, memory, and logical predicates are available in the CDCL proof library.

Verification results

At the first completed verification, the solver contained 362 lines of C code, with 2,275 lines of annotations and 14,977 lines of proof-library code. QCP generated 1,037 verification conditions, of which 253 were discharged through supplementary proofs. The corresponding Manual .v files contained 11,675 lines.

Lines of C code: 362
Annotation lines: 2,275
Proof-library lines: 14,977
Verification conditions: 1,037
Manual VCs: 253
Manual .v lines: 11,675

Statistics at the first completed verification. Subsequent cleanup in the public repository has changed the current counts. “Manual” denotes the supplementary proof path beyond automatic solving and includes work completed through human–AI collaboration.

The complete C implementation, QCP annotations, and Rocq proofs are publicly available with QCP 2.1.0 through the links at the top of this article.