DPLL(T)

DPLL(T) is the standard way to decide satisfiability of formulas that mix Boolean structure with a background theory $T$ , such as linear arithmetic or equality with uninterpreted functions^[2]^[1]. The formula's theory atoms, such as $x - y \leq 3$ , are abstracted as propositional variables, and a CDCL SAT solver, the DPLL part, searches for an assignment to them that satisfies the Boolean structure. A theory solver for $T$ checks whether the literals assigned so far are consistent in the theory. If they are not, it returns an explanation, a subset of them that is inconsistent, and the SAT solver adds the negation of the explanation as a learned clause, a theory lemma, and backjumps. It can also tell the SAT solver about literals that the current ones imply, which is theory propagation. The architecture was presented by Ganzinger, Hagen, Nieuwenhuis, Oliveras and Tinelli in 2004^[2] and described as an abstract transition system in 2006^[1]; it underlies nearly every SMT solver.

§ 01

The abstract procedure

Nieuwenhuis, Oliveras and Tinelli described DPLL and its extensions as rules that transform a state $M ∥ F$ , where $M$ is the sequence of assigned literals, some marked as decisions, and $F$ the set of clauses^[1]. The Boolean rules are those of CDCL: Decide adds an unassigned literal as a decision; UnitPropagate adds the last literal of a clause whose other literals are false; Backjump replaces the part of $M$ after some decision with a literal implied by a learned clause; Fail ends with unsatisfiability when a clause is false and there are no decisions. The theory adds:

T-Propagate adds a literal $ℓ$ of $F$ when $M ⊨_{T} ℓ$ . T-Learn adds a clause $C$ built from atoms of $F$ when $F ⊨_{T} C$ ; theory lemmas, the negations of explanations, are such clauses. T-Forget removes a learned clause. T-Backjump is Backjump with $⊨_{T}$ in place of propositional entailment. A run is correct whatever order the rules are applied in, which is what makes it possible to vary the strategy without changing the correctness argument^[1].

A small DPLL(T) implementation over integer atoms, generic in the theory. It backtracks chronologically; production solvers use CDCL with first-UIP learning.

(* DPLL(T): a DPLL search over Boolean atoms that consults a theory
   solver whenever unit propagation reaches a fixed point. Literals are
   non-zero integers: i stands for atoms.(i-1), -i for its negation. The
   theory accepts the assigned atoms or explains a conflict by a subset of
   them, whose negation is learned as a clause (a theory lemma). *)
module type THEORY = sig
  type atom
  type model
  val check : (atom * bool) list -> (model, (atom * bool) list) result
end
 
type stats = { mutable decisions : int; mutable conflicts : int; mutable lemmas : int;
               mutable checks : int; mutable tprops : int }
 
module Make (T : THEORY) = struct
  let trace = ref false
  let say fmt = Printf.ksprintf (fun s -> if !trace then print_endline s) fmt
 
  (* online: consult the theory at every propagation fixed point; if
     false, only when the assignment is total ("lemmas on demand").
     tprop: also ask the theory for implied atoms. *)
  let solve ?(online = true) ?(tprop = false) ?(name = string_of_int) (atoms : T.atom array) (input : int list list) =
    let n = Array.length atoms in
    let st = { decisions = 0; conflicts = 0; lemmas = 0; checks = 0; tprops = 0 } in
    let clauses = ref input in
    let value = Array.make (n + 1) 0 and level = Array.make (n + 1) 0 in
    let trail = ref [] and dl = ref 0 in
    let lv l = if value.(abs l) = 0 then 0 else if (value.(abs l) > 0) = (l > 0) then 1 else -1 in
    let assign l = value.(abs l) <- (if l > 0 then 1 else -1); level.(abs l) <- !dl; trail := l :: !trail in
    let show l = if l < 0 then "¬(" ^ name (-l) ^ ")" else name l in
    let index a = let i = ref 0 in Array.iteri (fun j x -> if x = a then i := j + 1) atoms; !i in
    let theory lits = st.checks <- st.checks + 1; T.check (List.map (fun l -> (atoms.(abs l - 1), l > 0)) lits) in
    let lemma expl = List.map (fun (a, b) -> if b then - (index a) else index a) expl in
    let rec propagate () =
      let conflict = ref None and changed = ref false in
      List.iter (fun c ->
          if !conflict = None && not (List.exists (fun l -> lv l = 1) c) then
            match List.filter (fun l -> lv l = 0) c with
            | [] -> conflict := Some c
            | [ l ] -> assign l; changed := true; say "  propagate %s" (show l)
            | _ -> ()) !clauses;
      match !conflict with
      | Some c -> Some c
      | None when !changed -> propagate ()
      | None when not online && Array.exists (( = ) 0) (Array.sub value 1 n) -> None
      | None ->
        (* ask the theory about the whole assignment *)
        match theory (List.rev !trail) with
        | Error expl ->
          let c = lemma expl in
          st.lemmas <- st.lemmas + 1; clauses := c :: !clauses;
          say "  theory conflict, learn %s" (String.concat " ∨ " (List.map show c));
          Some c
        | Ok _ when tprop ->
          (* theory propagation: an unassigned atom whose negation would
             be inconsistent is implied; learn the lemma that says so *)
          let implied = List.find_map (fun v ->
              if value.(v) <> 0 then None
              else List.find_map (fun l ->
                  match theory (List.rev (-l :: !trail)) with
                  | Error expl when List.mem (atoms.(v - 1), l < 0) expl -> Some (l, lemma expl)
                  | _ -> None) [ v; -v ]) (List.init n (fun i -> i + 1)) in
          (match implied with
           | Some (l, c) ->
             st.tprops <- st.tprops + 1; clauses := c :: !clauses;
             assign l; say "  theory propagates %s" (show l); propagate ()
           | None -> None)
        | Ok _ -> None
    in
    let result = ref None in
    while !result = None do
      match propagate () with
      | Some _ ->
        st.conflicts <- st.conflicts + 1;
        if !dl = 0 then result := Some None
        else begin
          (* undo the latest decision and assert its negation one level down *)
          let d = List.find (fun l -> level.(abs l) = !dl) (List.rev !trail) in
          trail := List.filter (fun l -> if level.(abs l) >= !dl then (value.(abs l) <- 0; false) else true) !trail;
          decr dl; assign (-d); say "backtrack: %s" (show (-d))
        end
      | None ->
        match List.find_opt (fun v -> value.(v) = 0) (List.init n (fun i -> i + 1)) with
        | None -> (match theory (List.rev !trail) with
            | Ok m -> result := Some (Some (m, List.rev !trail))
            | Error _ -> assert false)
        | Some v -> st.decisions <- st.decisions + 1; incr dl; assign v; say "decide %s" (show v)
    done;
    (Option.get !result, st)
end

§ 02

An example

Take difference-logic atoms $x - y \leq 0$ , $y - z \leq - 1$ , $z - x \leq 0$ and $w - y \leq 5$ , and the clauses stating that the third and second hold, and that the first or the fourth does.

Running the example with and without theory propagation.

module S = Dpllt.Make (Dl.Theory)
 
(* Atoms 1: x - y <= 0,  2: y - z <= -1,  3: z - x <= 0,  4: w - y <= 5.
   Clauses: (3), (2), (1 ∨ 4). *)
let atoms = [| { Dl.x = "x"; y = "y"; c = 0 }; { Dl.x = "y"; y = "z"; c = -1 };
               { Dl.x = "z"; y = "x"; c = 0 }; { Dl.x = "w"; y = "y"; c = 5 } |]
let clauses = [ [ 3 ]; [ 2 ]; [ 1; 4 ] ]

Running it.

without theory propagation:
  propagate z - x <= 0
  propagate y - z <= -1
decide x - y <= 0
  theory conflict, learn ¬(z - x <= 0) ∨ ¬(y - z <= -1) ∨ ¬(x - y <= 0)
backtrack: ¬(x - y <= 0)
  propagate w - y <= 5
model: w = 0, x = 0, y = -1, z = 0 (1 decision)
with theory propagation:
  propagate z - x <= 0
  propagate y - z <= -1
  theory propagates ¬(x - y <= 0)
  propagate w - y <= 5
model: w = 0, x = 0, y = -1, z = 0 (0 decisions)

The trail in both runs. Without theory propagation, the SAT solver decides x − y ≤ 0, the theory solver finds the cycle x → y → z → x of negative weight, and the lemma forces the opposite value. With theory propagation, the theory solver sees that the two unit atoms imply ¬(x − y ≤ 0) and asserts it directly.

§ 03

Lazy and eager

Before DPLL(T), two approaches competed. The eager approach translates the whole formula into an equisatisfiable propositional formula, encoding the relevant theory facts as clauses up front, and hands it to a SAT solver^[8]. The lazy approach, developed around 2002 in CVC, ICS, MathSAT and Verifun, lets a SAT solver find a propositional model first and asks a theory solver to check it, adding a lemma for each inconsistent model: "lemmas on demand"^[3]^[4]^[5]^[6]. DPLL(T) is the lazy approach made online: the theory solver is consulted during the search, after propagation, rather than only on complete models, so inconsistent partial assignments are cut off early.

Consulting the theory at every propagation fixed point against only on complete assignments, on job-shop scheduling instances.

(* Consulting the theory at every propagation fixed point (online), or
   only once the Boolean assignment is complete (offline, the "lemmas on
   demand" approach), on job-shop instances at their optimal makespan and
   one below it. *)
module S = Dpllt.Make (Dl.Theory)

Running it.

instance  makespan mode       decisions   lemmas   checks
3x3       23 yes   online            12        9       23
3x3       23 yes   offline           87       30       32
3x3       22 no    online             5        5       10
3x3       22 no    offline           87       31       31
4x3       27 yes   online            35       21       58
4x3       27 yes   offline          273       45       47
4x3       26 no    online            28       24       52
4x3       26 no    offline          418       88       88

Checking only complete assignments needs several times more decisions, since the search keeps extending assignments that are already inconsistent, and the gap grows with the instance. The number of theory checks is similar, but each offline check comes after much more wasted work.

§ 04

Theory propagation and explanations

How much a theory solver contributes depends on two capabilities. Theory propagation assigns atoms implied by the current literals, which is cheap for some theories, such as difference logic, where implied atoms correspond to paths in the constraint graph, and Nieuwenhuis and Oliveras showed that exhaustive propagation pays off there^[9]. Explanations must be small, since the learned clause contains one literal for each element; they must also be available for propagated literals, because conflict analysis resolves through them as it does through ordinary reasons^[1]^[7].

§ 05

History

Combining SAT solvers with decision procedures began with the eager encodings of the late 1990s^[8] and the lazy tools of 2002: CVC from Stanford^[6], ICS from SRI with lemmas on demand^[3], MathSAT from Trento^[4] and Verifun from Compaq^[5]. Ganzinger, Hagen, Nieuwenhuis, Oliveras and Tinelli introduced DPLL(T) at CAV 2004 with a modular interface between a DPLL engine and theory solvers^[2], and the 2006 Journal of the ACM paper gave the abstract transition-system view that became the standard account^[1]. The Barcelogic solver built on it did well in the first SMT competitions, and the design was adopted by Yices, Z3, cvc4 and their successors^[7].