All projects
Computational Thinking (Logic) · Durham University

Building a SAT solver: from brute force to DPLL

Mar 2023First yearPythonPropositional logicSATDIMACSAlgorithms

First-year logic coursework: a DIMACS CNF parser and a progression of satisfiability solvers in Python (exhaustive search, recursive branching, unit propagation and a DPLL-style solver), exercised on classic encodings such as 8-queens, the pigeonhole principle and the zebra puzzle.

The brief

Computational Thinking 2022/23 combined written logic questions (complete sets of connectives, validity in predicate logic) with a programming task: a sequence of Python functions over formulas in conjunctive normal form, with literals as integers (negative means negated) and clauses as lists, the same convention as the DIMACS format.

The progression

  • `load_dimacs` reads a DIMACS CNF file into a list of clauses.
  • `simple_sat_solve` tries every one of the 2ⁿ truth assignments, which is correct but exponential.
  • `branching_sat_solve` recursively assigns a variable true, then false, backtracking on failure.
  • `unit_propagate` repeatedly applies unit clauses: a clause with a single literal forces that literal, which simplifies every other clause.
  • `dpll_sat_solve` combines branching with unit propagation, in the style of the DPLL algorithm without pure-literal elimination.

From exhaustive search to DPLL

  1. 01
    Parse
    DIMACS CNF to a list of integer clauses
  2. 02
    Brute force
    Try all 2ⁿ assignments
  3. 03
    Branching
    Assign, recurse, backtrack
  4. 04
    Unit propagation
    Forced literals simplify the formula
  5. 05
    DPLL
    Branching with propagation

Benchmarks

The coursework came with standard encodings of increasing size, from a 3-variable test up to a Tower of Hanoi planning problem.

Benchmark instances: number of clauses

van der Waerden W(2,3), n = 8
40
Pigeonhole: 5 pigeons, 4 holes
85
Zebra puzzle
1,135
8-queens
1,464
Tower of Hanoi (planning)
4,934
Clause counts from each file's DIMACS header. The variable counts range from 16 (van der Waerden) to 718 (Tower of Hanoi).

Source: p cnf headers of the .txt instances in the coursework repository

Looking back

My DPLL was the weak point: rather than recursing on the simplified formula, it leaned on the brute-force search, so it couldn't reach the large instances. Today I'd have unit propagation return the simplified clause set, recurse on that with a variable-ordering heuristic, and add clause learning, the step that turns DPLL into a modern CDCL solver.

← Back to all projects
Building a SAT solver: from brute force to DPLL — Nichita Roscin