Difference logic

Difference logic is a fragment of linear arithmetic in which every atom has the form $x-y\le c$: the difference of two variables is bounded by a constant^[9]. Such constraints describe precedence and timing, as in "task $b$ starts at least 3 time units after task $a$", which is $a-b\le -3$. A conjunction of difference constraints can be decided in polynomial time by a graph algorithm: draw an edge from $y$ to $x$ of weight $c$ for each constraint; the constraints are satisfiable exactly when this graph has no cycle of negative total weight^[6]. The shortest-path distances then form a solution, and a negative cycle is a compact proof that none exists. SMT solvers decide arbitrary Boolean combinations of difference constraints by pairing a SAT search with such a graph-based theory solver^[1][2]. The fragment is known in SMT-LIB as QF_IDL over the integers and QF_RDL over the reals^[8].

Other bounds reduce to the basic form. A bound on one variable, $x\le c$, becomes $x-z\le c$ with a fresh variable $z$ standing for zero; since solutions can be shifted by a constant, any solution can be normalized to make $z=0$. An equality is two inequalities. Over the integers, the negation of $x-y\le c$ is $y-x\le -c-1$, which is again a difference constraint, so difference logic is closed under negation; over the reals, negation produces a strict inequality, which solvers handle with an infinitesimal.

For a set of constraints, build the constraint graph with a vertex per variable and an edge $y\stackrel{c}{\to }x$ for each constraint $x-y\le c$. Then

If there is a negative cycle, adding its constraints gives $0\le w<0$, where $w$ is the cycle's weight, since the variables cancel. If there is none, add a source with a 0-weight edge to every vertex; the shortest-path distances $d$ from it are finite and satisfy $d(x)\le d(y)+c$ for every edge, which is exactly $d(x)-d(y)\le c$: the distances are a solution^[6]. Over the integers they are integers, so the same test decides integer and real difference logic.

(* Difference logic over the integers: atoms x - y <= c. A set of such
   constraints is satisfiable exactly when the graph with an edge y -> x
   of weight c for each constraint has no negative cycle. *)
type atom = { x : string; y : string; c : int }          (* x - y <= c *)
 
let show a = Printf.sprintf "%s - %s <= %d" a.x a.y a.c
(* Over the integers, not (x - y <= c) is y - x <= -c - 1. *)
let negate a = { x = a.y; y = a.x; c = - a.c - 1 }
 
(* Bellman–Ford from a virtual source joined to every vertex by a
   0-weight edge. Returns a model, or the constraints on a negative cycle,
   which is the explanation of the conflict. *)
let check (cs : atom list) : ((string * int) list, atom list) result =
  let vs = List.sort_uniq compare (List.concat_map (fun a -> [ a.x; a.y ]) cs) in
  let dist = Hashtbl.create 16 and pred = Hashtbl.create 16 in
  List.iter (fun v -> Hashtbl.replace dist v 0) vs;
  let relax () =
    List.fold_left (fun changed a ->
        let d = Hashtbl.find dist a.y + a.c in
        if d < Hashtbl.find dist a.x then (Hashtbl.replace dist a.x d; Hashtbl.replace pred a.x a; Some a.x)
        else changed) None cs in
  let last = ref None in
  for _ = 1 to List.length vs do last := relax () done;
  match !last with
  | None -> Ok (List.map (fun v -> (v, Hashtbl.find dist v)) vs)
  | Some v ->
    (* walk back n steps to be sure to stand on the cycle, then collect it *)
    let v = ref v in
    for _ = 1 to List.length vs do v := (Hashtbl.find pred !v).y done;
    let start = !v in
    let rec collect u acc =
      let a = Hashtbl.find pred u in
      if a.y = start then a :: acc else collect a.y (a :: acc) in
    Error (collect start [])
 
(* As a DPLL(T) theory: a literal is an atom and a polarity. The
   explanation of a conflict is the set of literals on the cycle. *)
module Theory = struct
  type nonrec atom = atom
  type model = (string * int) list
  let check (lits : (atom * bool) list) =
    let tagged = List.map (fun (a, b) -> ((if b then a else negate a), (a, b))) lits in
    match check (List.map fst tagged) with
    | Ok m -> Ok m
    | Error cycle -> Error (List.map (fun c -> List.assoc c tagged) cycle)
end

open Dl
 
(* Four tasks with durations A 3, B 2, C 4, D 1; A precedes B and C,
   which both precede D. Start times sA .. sD, measured from z. *)
let precedes a da b = { x = a; y = b; c = - da }          (* a + da <= b *)
let tasks deadline = [
  { x = "z"; y = "sA"; c = 0 };                          (* A starts at 0 or later *)
  precedes "sA" 3 "sB"; precedes "sA" 3 "sC";
  precedes "sB" 2 "sD"; precedes "sC" 4 "sD";
  { x = "sD"; y = "z"; c = deadline - 1 } ]              (* D ends by the deadline *)

deadline 8: sA = 0, sB = 5, sC = 3, sD = 7
deadline 7: infeasible, negative cycle of weight -1:
    sA - sC <= -3
    z - sA <= 0
    sD - z <= 6
    sC - sD <= -4

The four constraints on the cycle are the explanation: they alone make the deadline infeasible, and the constraints involving task B play no part. In an SMT solver this explanation becomes a learned clause, and the shorter it is, the more of the search it prunes.

Conjunctions of difference constraints are easy; disjunctions make the problem NP-complete, since they can encode the requirement that two operations on the same machine do not overlap, $(a+d_a\le b)\vee (b+d_b\le a)$, and hence job-shop scheduling. Early approaches translated the whole formula into propositional logic, adding transitivity constraints between the atoms^[5]. The lazy approach now standard, DPLL(T), lets a SAT solver choose which atoms hold and asks the difference-logic solver whether the chosen conjunction is consistent; each negative cycle found becomes a clause that rules out that combination of atoms^[1].

(* A small job shop: three jobs, each an operation on machine 1 and one on
   machine 2 in a fixed order. Operations on the same machine must not
   overlap, which is a disjunction of two difference constraints. *)
module S = Dpllt.Make (Dl.Theory)
 
let ops = [ "o11", 1, 3; "o12", 2, 2; "o21", 2, 2; "o22", 1, 4; "o31", 1, 2; "o32", 2, 3 ]
let jobs = [ ("o11", "o12"); ("o21", "o22"); ("o31", "o32") ]
let dur o = let _, _, d = List.find (fun (n, _, _) -> n = o) ops in d
let before a b = { Dl.x = a; y = b; c = - (dur a) }          (* a ends before b starts *)
 
let solve makespan =
  let fixed = List.map (fun (a, b) -> before a b) jobs
              @ List.map (fun (o, _, _) -> { Dl.x = "z"; y = o; c = 0 }) ops
              @ List.map (fun (o, _, d) -> { Dl.x = o; y = "z"; c = makespan - d }) ops in
  let pairs = List.concat_map (fun (a, ma, _) -> List.filter_map (fun (b, mb, _) ->
      if ma = mb && a < b then Some (a, b) else None) ops) ops in
  let choice = List.concat_map (fun (a, b) -> [ before a b; before b a ]) pairs in
  let atoms = Array.of_list (fixed @ choice) in
  let nf = List.length fixed in
  let clauses = List.init nf (fun i -> [ i + 1 ])
                @ List.mapi (fun k _ -> [ nf + (2 * k) + 1; nf + (2 * k) + 2 ]) pairs in
  S.solve atoms clauses

makespan 12: feasible (11 decisions, 6 theory lemmas)  o11@0 o12@3 o21@5 o22@7 o31@5 o32@7
makespan 11: feasible (11 decisions, 6 theory lemmas)  o11@0 o12@3 o21@5 o22@7 o31@5 o32@7
makespan 10: feasible (10 decisions, 6 theory lemmas)  o11@0 o12@3 o21@1 o22@5 o31@3 o32@5
makespan  9: feasible (10 decisions, 6 theory lemmas)  o11@0 o12@3 o21@1 o22@5 o31@3 o32@5
makespan  8: infeasible (10 decisions, 9 theory lemmas)

The optimal makespan is 9, which is also the total processing time on machine 1, so the schedule keeps that machine busy without a break.

Running Bellman–Ford from scratch at every step is wasteful. Practical solvers keep the constraint graph and a solution between calls, and when a new constraint arrives, they update only the part of the solution it invalidates, which detects a new negative cycle in time roughly proportional to the affected vertices^[2]. They also perform theory propagation: a constraint $x-y\le c$ is implied by the asserted ones if there is a path from $y$ to $x$ of weight at most $c$, and asserting such implied atoms early, with the path as explanation, saves the SAT solver from guessing them^[1]. Nieuwenhuis and Oliveras showed that exhaustive theory propagation pays off for difference logic^[1].

Difference constraints are also the language of clock constraints in timed automata. Dill's difference bound matrices represent a convex set of clock valuations as the matrix of tightest bounds $x_i-x_j\le c_{ij}$, closed under shortest paths, and operations such as letting time pass, resetting a clock or intersecting with a guard are matrix updates^[4]. Model checkers for timed automata, such as UPPAAL, are built on them.

The connection between difference constraints and shortest paths follows from the Bellman–Ford algorithm of the 1950s^[7] and is textbook material^[6]. Pratt studied the theory of separation constraints in 1977 and showed that it is easy on its own but hard in combination with others^[3]. Dill introduced difference bound matrices for timing verification in 1989^[4]. With the development of SMT in the early 2000s, difference logic became one of its first practical theories: Strichman, Seshia and Bryant reduced it to SAT in 2002^[5], Nieuwenhuis and Oliveras built it into DPLL(T) with exhaustive propagation in 2005^[1], and Cotton and Maler gave incremental algorithms in 2006^[2].

• Theory solverIn an SMT solver, a theory solver decides whether a conjunction of literals of one theory, such as linear arithmetic or equality with uninterpreted functions, is consistent. The SAT search asserts literals to it incrementally and asks it to check them; on inconsistency it returns an explanation, a small subset of the asserted literals that is already inconsistent, which the SAT search learns as a clause. A theory solver must also undo assertions when the search backtracks, and it may propagate literals that the asserted ones imply. The quality of explanations and propagation largely determines the solver's performance.
• SMTSatisfiability modulo theories (SMT) is the problem of deciding whether a first-order formula is satisfiable when some of its symbols are interpreted by background theories, such as integer or real arithmetic, bit-vectors, arrays and uninterpreted functions. SMT solvers such as Z3 and cvc5 combine a SAT solver, which handles the Boolean structure, with specialized decision procedures for the theories, usually in the DPLL(T) architecture. They read the standard SMT-LIB language and are the reasoning engines of program verifiers, symbolic execution tools, test generators and many other analysis tools.
• DPLL(T)DPLL(T) is the architecture of lazy SMT solvers: a CDCL SAT solver searches over the Boolean structure of a formula, treating each theory atom as a propositional variable, and a theory solver for T checks the consistency of the atoms it assigns. When the theory solver finds the assigned literals inconsistent, it returns an explanation, whose negation the SAT solver learns as a clause before backjumping; it may also propagate literals the assignment implies. The approach separates a generic engine from pluggable theory solvers and is used by nearly all SMT solvers, including Z3, cvc5 and Yices.
• Nelson–Oppen combinationThe Nelson–Oppen method decides satisfiability of quantifier-free formulas that mix several theories with disjoint signatures, such as linear arithmetic and uninterpreted functions, using only a decision procedure for each theory. The formula is first purified, by naming mixed subterms with fresh variables, so that every literal belongs to one theory; the theory solvers then agree on which of their shared variables are equal, either by propagating the equalities each entails (enough for convex theories) or by searching over all arrangements of the shared variables. It is complete for theories that are stably infinite, and it is how SMT solvers combine their theory solvers.
• Simplex methodThe simplex method solves linear programs, maximizing a linear function subject to linear inequalities, by walking along the edges of the feasible polyhedron from vertex to vertex, each step improving the objective, until no neighbouring vertex is better. Each step is a pivot on a tableau. It is fast in practice and in smoothed analysis, but takes exponential time on the Klee-Minty cubes with Dantzig's pivoting rule, and needs a rule such as Bland's to avoid cycling on degenerate problems. Its final tableau also gives a solution of the dual program, certifying optimality.
• Fourier–Motzkin eliminationFourier–Motzkin elimination removes a variable from a system of linear inequalities by combining every inequality that bounds the variable from below with every inequality that bounds it from above. The result has a solution exactly when the original system does, over the real or rational numbers, and describes the projection of the solution set. Eliminating all variables decides satisfiability, and back-substitution recovers a solution, but the number of inequalities can grow doubly exponentially.

• Implementing SAT in OCaml Part 4A real linear-arithmetic fragment: difference logic atoms x - y <= k, decided by Bellman-Ford negative-cycle detection with explanations.

1. [1]R. Nieuwenhuis, A. Oliveras, “DPLL(T) with exhaustive theory propagation and its application to difference logic”, CAV (2005).
2. [2]S. Cotton, O. Maler, “Fast and flexible difference constraint propagation for DPLL(T)”, SAT, Lecture Notes in Computer Science 4121 (2006).
3. [3]V. R. Pratt, “Two easy theories whose combination is hard”, technical report, Massachusetts Institute of Technology (1977).
4. [4]D. L. Dill, “Timing assumptions and verification of finite-state concurrent systems”, Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407 (1989).
5. [5]O. Strichman, S. A. Seshia, R. E. Bryant, “Deciding separation formulas with SAT”, CAV (2002).
6. [6]T. H. Cormen, C. E. Leiserson, R. L. Rivest, C. Stein, Introduction to Algorithms, §24.4 “Difference constraints and shortest paths”, MIT Press (3rd ed., 2009).
7. [7]R. Bellman, “On a routing problem”, Quarterly of Applied Mathematics 16 (1958).
8. [8]C. Barrett, P. Fontaine, C. Tinelli, The SMT-LIB Standard, version 2.6 (2017).
9. [9]D. Kroening, O. Strichman, Decision Procedures: An Algorithmic Point of View, ch. 5, Springer (2nd ed., 2016).

last updated 28 September 2026