Theory solver

A theory solver is the component of an SMT solver that understands one background theory^[1]^[2]. The Boolean search of DPLL(T) treats every theory atom, such as $x - y \leq 3$ or $f (a) = b$ , as an opaque propositional variable, and relies on the theory solver to tell it which combinations of truth values make sense. For this the theory solver needs only to decide conjunctions of literals, which is often far easier than deciding arbitrary formulas: a conjunction of difference constraints is a shortest-path problem, and a conjunction of equalities is congruence closure. The search asserts literals as it assigns them, asks whether they are consistent, and retracts them when it backtracks. When they are inconsistent, the theory solver returns an explanation, a subset of the asserted literals that is already inconsistent, and its negation becomes a clause that the search learns, a theory lemma. A theory solver can also report literals that the asserted ones imply, theory propagation, saving the search from guessing them^[5].

§ 01

The interface

The messages between the SAT search and a theory solver. Assertions and checks flow right; conflicts with their explanations and implied atoms flow back; backtracking pops the theory solver's state to an earlier decision level.

The exact interface differs between solvers, but the operations are the same^[1]^[2]:

Assert adds a literal to the theory solver's set. Check decides whether the set is consistent; solvers often distinguish a cheap partial check, run after every propagation, from a complete final check, run when the Boolean assignment is total. Explain returns, for a conflict or a propagated literal, the asserted literals that justify it. Backtrack returns to the state at an earlier decision level. Model produces values for the theory's variables when the final check succeeds, and in combinations of theories the solver must also report equalities between shared variables that it entails^[8]^[10].

The theory interface used by a small DPLL(T) implementation: the theory receives the assigned atoms and returns a model or an explanation.

(* 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

§ 02

Explanations

An explanation is correct if it is inconsistent on its own; it is useful if it is small. The learned clause contains one literal per element of the explanation, and a short clause rules out every assignment that contains the same few literals, whereas a long one rules out little more than the current assignment. Minimal explanations, from which no literal can be dropped, are ideal but not always cheap to compute. For difference logic, a negative cycle in the constraint graph is a natural explanation^[5]; for congruence closure, the equations along the proof of the violated equality^[4]; for linear arithmetic, the rows of the simplex tableau that witness infeasibility^[3].

A job-shop instance solved at its optimal makespan and one below, with three difference-logic theory solvers: one that explains conflicts by a negative cycle, one that blames every asserted literal, and the first with theory propagation.

(* The same DPLL(T) search with three difference-logic theory solvers:
   one that explains a conflict by its negative cycle, one that blames
   every asserted literal, and the first with theory propagation. *)
module Cycle = Dpllt.Make (Dl.Theory)
module Blame_all = Dpllt.Make (struct
    include Dl.Theory
    let check lits = match Dl.Theory.check lits with Ok m -> Ok m | Error _ -> Error lits
  end)

Decisions, learned theory lemmas and theory checks.

makespan   theory solver               result  decisions  lemmas   checks
32         cycle explanation         feasible         55      30       87
32         blame everything          feasible         55      30       87
32         cycle + propagation       feasible          8       0     1358
31         cycle explanation               no        161      75      236
31         blame everything                no       2633    2634     5267
31         cycle + propagation             no          3       4     1626

When a schedule exists, the first two solvers behave alike, since the search finds it before explanations matter. When none exists, blaming every literal makes the search enumerate far more assignments, 2,633 decisions against 161, because each lemma excludes only the exact assignment that failed. Theory propagation nearly removes the search, at the price of many more theory checks, because the implementation here finds implied atoms by trial; real solvers compute them directly from their data structures, for instance from shortest paths in the constraint graph^[5].

§ 03

Incrementality and backtracking

The SAT search asserts one literal at a time and backtracks often, so a theory solver that starts from scratch at every check wastes most of its work. Practical solvers keep their state between calls and update it for each new literal: a congruence-closure solver merges two classes, a difference-logic solver repairs the potential function around one new edge, and a simplex-based solver adjusts the bounds of one variable and pivots only if needed^[3]. Backtracking must restore the state of an earlier level cheaply; solvers keep a trail of changes and undo them in reverse, or, like the simplex solver of Dutertre and de Moura, arrange that backtracking only relaxes bounds and never needs to undo pivots^[3].

§ 04

Common theories

The theories most used in practice have well-understood solvers^[2]^[9]. Equality with uninterpreted functions uses congruence closure^[4]. Linear real arithmetic uses a variant of the simplex method specialized for incremental bound changes^[3]; linear integer arithmetic adds branch-and-bound and cutting planes on top of it. Difference logic uses graph algorithms. Fixed-width bit-vectors are usually handled by bit-blasting into propositional clauses. Arrays are handled by instantiating their read-over-write axioms lazily, as lemmas when a candidate model violates them. Z3 and cvc5 provide dozens of such solvers^[6].

§ 05

History

Decision procedures for conjunctions of literals in particular theories predate SMT; Nelson and Oppen's combination method of 1979 already assumed theory solvers that report entailed equalities^[8]. The modern interface took shape with DPLL(T), presented by Ganzinger, Hagen, Nieuwenhuis, Oliveras and Tinelli in 2004^[7] and formalized by Nieuwenhuis, Oliveras and Tinelli in 2006^[1], which separated a generic DPLL engine from theory solvers that assert, check, explain and backtrack. Exhaustive theory propagation for difference logic^[5], proof-producing congruence closure^[4] and the incremental simplex of Dutertre and de Moura^[3] followed, and model-based theory combination replaced eager equality propagation in Z3^[10]^[6].