DPLL

Davis-Putnam-Logemann-Loveland: the backtracking search underneath every classical SAT solver. Propagate units, and if that produces no conflict pick an unassigned variable, assign it, and recurse; on conflict undo the most recent decision and try the other value. Correct, complete, and exponential on the instances designed to hurt it.

Propagate units; if that yields a conflict, backtrack; otherwise pick an unassigned variable, assign it, and recurse. That is the whole algorithm, and it is still the skeleton inside every complete SAT solver.

let rec dpll cs a =
  match propagate cs a with
  | None -> None                                     (* conflict *)
  | Some a ->
    let vars = List.sort_uniq compare (List.map abs (List.concat cs)) in
    (match List.find_opt (fun v -> not (List.mem_assoc v a)) vars with
     | None -> Some a                                (* total, conflict-free *)
     | Some v ->
       (match dpll cs ((v, true) :: a) with
        | Some a -> Some a
        | None -> dpll cs ((v, false) :: a)))        (* try the other value *)

dpll [[1;2]; [-1;2]; [-2]] []   ->  UNSAT
dpll [[1;2]; [-1;3]] []         ->  1=true 2=true 3=true

It is sound and complete, and it is also the reason CDCL exists. On conflict it undoes exactly one decision and forgets everything it learned in the process, so the same conflict can be rediscovered exponentially many times along different paths.

CDCL · Unit propagation · SAT

Pure literal elimination

• Implementing SAT in OCaml Part 1CNF, unit propagation, a full recursive DPLL solver, pure literal elimination, a DIMACS parser, and a command-line driver.