Algorithms for Satisfiability Modulo Theories IA085: Satisfiability and Automated Reasoning Martin Jonáš FI MUNI, Spring 2024 Last time • overview of basic notions of first-order logic and satisfiabilty modulo theories • overview of practically used theories 1 / 29 Terminology • T-valid formula = T-lemma • T-satisfiable formula = T-consistent formula 2 / 29 Solving Satisfiability Modulo Theories Two approaches eager encode the input SMT formula into an equisatisfiable SAT formula and use a SAT solver lazy try checking individual Boolean assignments to the input SMT formula one by one 3 / 29 Eager algorithms Eager algorithms Encode the input SMT formula into an equisatisfiable SAT formula and use a SAT solver. Small-domain encoding • prove a result “if φ has a model, it has a model of size at most k = f(|φ|)” • express the set {1, . . . , k} and all the operations by a SAT formula • example: equality (f = linear), linear arithmetic (f = exponential) Encoding of axioms • instantiate all the necessary axioms of the theory and add them to the formula 4 / 29 Encoding axioms: Theory of Equality a = b ∧ (b = c ∨ b ̸= d) ∧ a ̸= c ∧ b = d eq{a,b} ∧ (eq{b,c} ∨ ¬eq{b,d}) ∧ ¬eq{a,c} ∧ eq{b,d} where • eq{x,y} are Boolean variables and • eq{x,y} and eq{y,x} are the same variable. 5 / 29 Encoding axioms: Theory of Equality a = b ∧ (b = c ∨ b ̸= d) ∧ a ̸= c ∧ b = d eq{a,b} ∧ (eq{b,c} ∨ ¬eq{b,d}) ∧ ¬eq{a,c} ∧ eq{b,d} where • eq{x,y} are Boolean variables and • eq{x,y} and eq{y,x} are the same variable. Are we done? 5 / 29 Encoding axioms: Theory of Equality a = b ∧ (b = c ∨ b ̸= d) ∧ a ̸= c ∧ b = d eq{a,b} ∧ (eq{b,c} ∨ ¬eq{b,d}) ∧ ¬eq{a,c} ∧ eq{b,d} where • eq{x,y} are Boolean variables and • eq{x,y} and eq{y,x} are the same variable. Are we done? Add transitivity and reflexivity • for each added eq{x,y} and eq{y,z}, add conjunct (eq{x,y} ∧ eq{y,z}) → eq{x,z} • replace each added eq{x,x} by ⊤ 5 / 29 Encoding axioms: Theory of Equality and Uninterpreted Functions x = v ∧ y = g(z) ∧ f(g(x)) ̸= f(y) ∧ z = v x = v ∧ y = resg(z) ∧ resf(g(x)) ̸= resf(y) ∧ z = v where resf(t) and resg(t) are new variables Are we done? 6 / 29 Encoding axioms: Theory of Equality and Uninterpreted Functions x = v ∧ y = g(z) ∧ f(g(x)) ̸= f(y) ∧ z = v x = v ∧ y = resg(z) ∧ resf(g(x)) ̸= resf(y) ∧ z = v where resf(t) and resg(t) are new variables Are we done? Add congruences • for each added resf(t1) and resf(t2), add conjunct (t1 = t2) → (resf(t1) = resf(t2)) • similarly for functions of higher arity: (t1 = t2 ∧ s1 = s2) → (resh(t1,s1) = resh(t2,s2)) • repeat until fixed point 6 / 29 Encoding axioms: Theory of Equality and Uninterpreted Functions The above procedure • removes uninterpreted functions by adding new variables and congruences • reduction of UF to the theory of equality • known as Ackermann’s reduction 7 / 29 Eager algorithms • usually poor performance, interesting only theoretically • nowadays almost never used in practice • one exception: theory of fixed-size bit-vectors (next time) 8 / 29 Lazy algorithms Lazy algorithms SMT formula = Boolean structure + theory literals Combine • SAT solver to perform the Boolean search • Theory solver (T-solver) to check satisfiability of conjunctions of T-literals In the rest of the lecture assume that we have a T-solver for the theory T. 9 / 29 Lazy algorithms Note • all following examples use the LRA theory • because the structure is fixed, instead of (A, µ) |= φ, write only µ |= φ (and similar) 10 / 29 Propositional abstraction Propositional abstraction • replace each atomic subformula ψ in the formula φ by a new Boolean variable • resulting formula φP • denote the mapping by two functions T 2B and B2T Example φ = x = 1 ∧ (y < 3 ∨ x + y = 4) ∧ (¬(y < 3) ∨ x + y = 10) φP = A1 ∧ (A2 ∨ A3) ∧ (¬A2 ∨ A4) where T 2B(x = 1) = A1 and B2T (¬A2) = ¬(y < 3) 11 / 29 Propositional abstraction Theorem If the propositional abstraction φP is unsatisfiable, the original formula φ is T-unsatisfiable. Proof. If µ is a T-model of the original formula φ, then µP defined by µ(Ai) = B2T (Ai) µ is a propositional model of φP . The converse does not hold. 12 / 29 Propositional abstraction Each propositional assignment µ of φP corresponds to a conjunction of T-literals µT = ∧ v∈Vars,µ(v)=⊤ B2T (v) ∧ ∧ v∈Vars,µ(v)=⊥ ¬B2T (v) Example For φ = x = 1 ∧ (y < 3 ∨ x + y = 4) ∧ (¬(y < 3) ∨ x + y = 10) φP = A1 ∧ (A2 ∨ A3) ∧ (¬A2 ∨ A4) and µ(A1) = ⊤, µ(A2) = ⊥, µ(A3) = ⊤ µT = (x = 1) ∧ ¬(y < 3) ∧ (x + y = 4) 13 / 29 Offline Lazy SMT solving – schema CDCL solver T-solver φ SAT/UNSAT µT SAT/UNSAT 14 / 29 Offline Lazy SMT solving – algorithm 1 offline_smt(formula φ): 2 φP ← T 2B(φ) 3 while check_sat(φP ) == SAT { 4 µ = get_model(φP ) 5 if check_theory(µT ) == SAT { 6 return SAT 7 } else { 8 φP ← φP ∧ ¬µ 9 } 10 } 11 return UNSAT 15 / 29 Offline Lazy SMT solving – example φ = x = 1 ∧ (y < 3 ∨ y > 5) ∧ (x + y = 4 ∨ y = 6) B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} 16 / 29 Offline Lazy SMT solving – example φ = x = 1 ∧ (y < 3 ∨ y > 5) ∧ (x + y = 4 ∨ y = 6) B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} 16 / 29 Offline Lazy SMT solving – example φ = x = 1 ∧ (y < 3 ∨ y > 5) ∧ (x + y = 4 ∨ y = 6) B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} µ = {A1, A2, ¬A3, A4, ¬A5} µP = x = 1∧y < 3∧¬(y > 5)∧x+y = 4∧¬(y = 6) 16 / 29 Offline Lazy SMT solving – example φ = x = 1 ∧ (y < 3 ∨ y > 5) ∧ (x + y = 4 ∨ y = 6) B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} µ = {A1, A2, ¬A3, A4, ¬A5} µP = x = 1∧y < 3∧¬(y > 5)∧x+y = 4∧¬(y = 6) T-unsatisfiable 16 / 29 Offline Lazy SMT solving – example φ = x = 1 ∧ (y < 3 ∨ y > 5) ∧ (x + y = 4 ∨ y = 6) B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, A3, ¬A4, A5} µ = {A1, A2, ¬A3, A4, ¬A5} µP = x = 1∧y < 3∧¬(y > 5)∧x+y = 4∧¬(y = 6) T-unsatisfiable 16 / 29 Offline Lazy SMT solving – example φ = x = 1 ∧ (y < 3 ∨ y > 5) ∧ (x + y = 4 ∨ y = 6) B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, A3, ¬A4, A5} µ = {A1, A2, ¬A3, A4, A5} µP = x = 1 ∧ y < 3 ∧ ¬(y > 5) ∧ x + y = 4 ∧ y = 6 16 / 29 Offline Lazy SMT solving – example φ = x = 1 ∧ (y < 3 ∨ y > 5) ∧ (x + y = 4 ∨ y = 6) B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, A3, ¬A4, A5} µ = {A1, A2, ¬A3, A4, A5} µP = x = 1 ∧ y < 3 ∧ ¬(y > 5) ∧ x + y = 4 ∧ y = 6 T-unsatisfiable 16 / 29 Offline Lazy SMT solving – example φ = x = 1 ∧ (y < 3 ∨ y > 5) ∧ (x + y = 4 ∨ y = 6) B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, A3, ¬A4, A5} {¬A1, ¬A2, A3, ¬A4, ¬A5} µ = {A1, A2, ¬A3, A4, A5} µP = x = 1 ∧ y < 3 ∧ ¬(y > 5) ∧ x + y = 4 ∧ y = 6 T-unsatisfiable 16 / 29 Offline Lazy SMT solving – example φ = x = 1 ∧ (y < 3 ∨ y > 5) ∧ (x + y = 4 ∨ y = 6) B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, A3, ¬A4, A5} {¬A1, ¬A2, A3, ¬A4, ¬A5} µ = {A1, A2, ¬A3, ¬A4, A5} µP = x = 1∧y < 3∧¬(y > 5)∧¬(x+y = 4)∧y = 6 16 / 29 Offline Lazy SMT solving – example φ = x = 1 ∧ (y < 3 ∨ y > 5) ∧ (x + y = 4 ∨ y = 6) B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, A3, ¬A4, A5} {¬A1, ¬A2, A3, ¬A4, ¬A5} µ = {A1, A2, ¬A3, ¬A4, A5} µP = x = 1∧y < 3∧¬(y > 5)∧¬(x+y = 4)∧y = 6 T-unsatisfiable 16 / 29 Offline Lazy SMT solving – example φ = x = 1 ∧ (y < 3 ∨ y > 5) ∧ (x + y = 4 ∨ y = 6) B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, A3, ¬A4, A5} {¬A1, ¬A2, A3, ¬A4, ¬A5} {¬A1, ¬A2, A3, A4, ¬A5} µ = {A1, A2, ¬A3, ¬A4, A5} µP = x = 1∧y < 3∧¬(y > 5)∧¬(x+y = 4)∧y = 6 T-unsatisfiable 16 / 29 Offline Lazy SMT solving – example φ = x = 1 ∧ (y < 3 ∨ y > 5) ∧ (x + y = 4 ∨ y = 6) B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, A3, ¬A4, A5} {¬A1, ¬A2, A3, ¬A4, ¬A5} {¬A1, ¬A2, A3, A4, ¬A5} µ = {A1, ¬A2, A3, ¬A4, A5} µP = x = 1∧¬(y < 3)∧y > 5∧¬(x+y = 4)∧y = 6 16 / 29 Offline Lazy SMT solving – example φ = x = 1 ∧ (y < 3 ∨ y > 5) ∧ (x + y = 4 ∨ y = 6) B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, A3, ¬A4, A5} {¬A1, ¬A2, A3, ¬A4, ¬A5} {¬A1, ¬A2, A3, A4, ¬A5}} µ = {A1, ¬A2, A3, ¬A4, A5} µP = x = 1∧¬(y < 3)∧y > 5∧¬(x+y = 4)∧y = 6 T-satisfiable 16 / 29 Offline Lazy SMT solving Downsides • the SAT solver is executed from scratch every time • propositional models are blocked one at time • theory reasoning is applied only for complete assignments 17 / 29 CDCL(T) CDCL(T) • tight integration of a CDCL-based SAT solver and a theory solver • theory solver can explain conflicts and guide the search of the SAT solver • basis of most of modern SMT solvers (CVC5, MathSAT, Yices, Z3, . . .) 18 / 29 CDCL(T) – schema CDCL solver T-solver φ SAT/UNSAT assigned variable backtracked variable T-conflict+explanation T-propagation T-lemma 19 / 29 Conflict Explanation • if the T-solver detects a conflict in the Boolean assignment µ = {l1, . . . , lk}, it can compute its subset µ′ ⊆ µ such that µ′ |=T ⊥ • instead of learning ∨l∈µ¬l, the SAT solver can learn ∨l∈µ′ ¬l 20 / 29 Conflict Explanation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} 21 / 29 Conflict Explanation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} 21 / 29 Conflict Explanation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} µ = {A1, A2, ¬A3, A4, ¬A5} µP = x = 1∧y < 3∧¬(y > 5)∧x+y = 4∧¬(y = 6) 21 / 29 Conflict Explanation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} µ = {A1, A2, ¬A3, A4, ¬A5} µP = x = 1∧y < 3∧¬(y > 5)∧x+y = 4∧¬(y = 6) T-unsatisfiable reason {A1, A2, A4} 21 / 29 Conflict Explanation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, ¬A4} µ = {A1, A2, ¬A3, A4, ¬A5} µP = x = 1∧y < 3∧¬(y > 5)∧x+y = 4∧¬(y = 6) T-unsatisfiable reason {A1, A2, A4} 21 / 29 Conflict Explanation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, ¬A4} µ = {A1, A2, ¬A3, ¬A4, A5} µP = x = 1∧y < 3∧¬(y > 5)∧¬(x+y = 4)∧y = 6 21 / 29 Conflict Explanation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, ¬A4} µ = {A1, A2, ¬A3, ¬A4, A5} µP = x = 1∧y < 3∧¬(y > 5)∧¬(x+y = 4)∧y = 6 T-unsatisfiable reason {A2, A5} 21 / 29 Conflict Explanation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, ¬A4} {¬A2, ¬A5} µ = {A1, A2, ¬A3, ¬A4, A5} µP = x = 1∧y < 3∧¬(y > 5)∧¬(x+y = 4)∧y = 6 T-unsatisfiable reason {A2, A5} 21 / 29 Conflict Explanation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, ¬A4} {¬A2, ¬A5} µ = {A1, ¬A2, A3, ¬A4, A5} µP = x = 1∧¬(y < 3)∧y > 5∧¬(x+y = 4)∧y = 6 21 / 29 Conflict Explanation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2, ¬A4} {¬A2, ¬A5}} µ = {A1, ¬A2, A3, ¬A4, A5} µP = x = 1∧¬(y < 3)∧y > 5∧¬(x+y = 4)∧y = 6 T-satisfiable 21 / 29 Theory propagation • SAT solver notifies the T-solver about all variable assignments/backtracking • T-solver knows the currently assigned literals µT • T-solver can detect T-entailed literals µT |=T l and propagate them For the backtracking • T-solver must be able to provide explanations of the propagations • for each T-propagated literal µT |= l, an explanation µ′ ⊆ µT such that µ′ |=T l 22 / 29 Theory propagation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} } SAT solver trail T-solver assignment 23 / 29 Theory propagation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} } SAT solver trail Aup 1 T-solver assignment x = 1 23 / 29 Theory propagation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} } SAT solver trail Aup 1 , Ad 2 T-solver assignment x = 1 y < 3 23 / 29 Theory propagation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} } SAT solver trail Aup 1 , Ad 2 , ¬Atp 3 T-solver assignment x = 1 y < 3 ¬(y > 5) 23 / 29 Theory propagation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} } SAT solver trail Aup 1 , Ad 2 , ¬Atp 3 , ¬Atp 4 T-solver assignment x = 1 y < 3 ¬(y > 5) ¬(x + y = 4) 23 / 29 Theory propagation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} } SAT solver trail Aup 1 , Ad 2 , ¬Atp 3 , ¬Atp 4 , ¬Atp 5 T-solver assignment x = 1 y < 3 ¬(y > 5) ¬(x + y = 4) ¬(y = 6) 23 / 29 Theory propagation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} } SAT solver trail Aup 1 , Ad 2 , ¬Atp 3 , ¬Atp 4 , ¬Atp 5 T-solver assignment x = 1 y < 3 ¬(y > 5) ¬(x + y = 4) ¬(y = 6) 23 / 29 Theory propagation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2} } SAT solver trail Aup 1 , Ad 2 , ¬Atp 3 , ¬Atp 4 , ¬Atp 5 T-solver assignment x = 1 y < 3 ¬(y > 5) ¬(x + y = 4) ¬(y = 6) 23 / 29 Theory propagation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2} } SAT solver trail Aup 1 , ¬Abj 2 T-solver assignment x = 1 ¬(y < 3) 23 / 29 Theory propagation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2} } SAT solver trail Aup 1 , ¬Abj 2 , Aup 3 T-solver assignment x = 1 ¬(y < 3) (y > 5) 23 / 29 Theory propagation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2} } SAT solver trail Aup 1 , ¬Abj 2 , Aup 3 , ¬Atp 4 T-solver assignment x = 1 ¬(y < 3) (y > 5) ¬(x + y = 4) 23 / 29 Theory propagation: Example B2T (A1) = x = 1, B2T (A2) = y < 3, B2T (A3) = y > 5, B2T (A4) = x + y = 4, B2T (A5) = y = 6 φP = {{A1}, {A2, A3}, {A4, A5} {¬A1, ¬A2} } SAT solver trail Aup 1 , ¬Abj 2 , Aup 3 , ¬Atp 4 , Aup 5 T-solver assignment x = 1 ¬(y < 3) (y > 5) ¬(x + y = 4) y > 5 23 / 29 Early pruning • T-solver knows the currently assigned literals µT • if µT |=T ⊥, declare conflict before setting all literals For correctness • needs to provide explanations of the conflicts • can perform cheaper approximate check → does not have to detect all inconsistencies • the expensive full check needs to be performed only for the complete assignments 24 / 29 Interface of T-solver T-solver can be instantiated arbitrarily, but it should • handle assignment of literal values efficiently • backtrack efficiently • provide reasons for theory conflicts It further can • perform theory propagation (identify implied literals) • perform early pruning (identify theory conflicts during the search) 25 / 29 Interface of T-solver Possible interface of the T-solver • void notifyAtom(lit) • void assignLiteral(lit) • void push() • void pop() • result checkSat() • option checkSat_approx() • list getConflictReason() • option getPropagatedLiteral() • list getExplanation(lit) 26 / 29 Other improvements • normalize T-literals – (x > y) ¬(x ≤ y) – (y + 3 + x) x + y + 3 • eagerly learn some interesting T-lemmas – if the formula contains x = 0 and x = 1 – add T-lemma ¬(x = 0) ∨ ¬(x = 1) before solving • pure literal filtering – if the formula contains a literal l only positively and the current assignment contains ¬l, do not send ¬l to the T-solver • splitting on demand – when T-solver wants to do a case split, it can add a new T-lemma corresponding to the split to the SAT solver – can introduce new T-literals and new Boolean variables – (x + y < 0) ∨ (x + y ≥ 0) – case split will be performed as part of the propositional search 27 / 29 Modern SMT solvers CDCL solver LRA-solver LIA-solver BV-solver UF-solver . . . Theory combination 28 / 29 Next time • theory solvers for selected theories 29 / 29