Combination of Theories
IA085: Satisfiability and Automated Reasoning
Martin Jonáš
FI MUNI, Spring 2024
Last time
• theory solvers for UF and difference logic
• sketches of ideas of other theory solvers
1 / 39
Assumptions
• all formulas are quantifier-free (necessary)
• all formulas are conjunctions of literals (not necessary)
2 / 39
Combination of theories
Motivation
Practical applications combine several theories
x = y + 2 ∧ f(x − 1) ̸= f(y + 1) ∨ read(a, x) = read(a, y)
• formula over TLIA, TUF, and TA
3 / 39
Motivation
Practical applications combine several theories
x = y + 2 ∧ f(x − 1) ̸= f(y + 1) ∨ read(a, x) = read(a, y)
• formula over TLIA, TUF, and TA
• it is impractical to create a new T solver for each combination of theories
Goal
• construct a solver for the combined theory modularly from existing T-solvers
for the individual theories
3 / 39
Goal
CDCL solver
LRA-solver
LIA-solver
BV-solver
UF-solver
. . .
Theory combination
4 / 39
Combined theory
Setup
• T1 over signature Σ1
• T2 over signature Σ2
• are signature disjoint, i.e., Σ1 ∩ Σ2 = {=}
Want to define combined theory T1 ⊕ T2 over Σ = Σ1 ∪ Σ2.
5 / 39
Combined theory: axiom-based view
If
• T1 is given by axioms A1 and
• T2 is given by axioms A2
then
• T1 ⊕ T2 is given by axioms A1 ∪ A2
6 / 39
Combined theory: model-based view
Let
• A = (A, (_)A) be ΣA-structure
• ΣB ⊆ ΣA
ΣB reduct of A
• ΣB structure B = (A, (_)B) where
• fB = fA for all f ∈ Σf
B
• PB = PA for all P ∈ Σp
B
• also denoted A ΣB
Example
{+, ≤}-reduct of (Z, +, ×, ≤) is (Z, +, ≤)
7 / 39
Combined theory: model-based view
Σ-structures A and B are elementarily equivalent if they satisfy exactly the same
Σ-formulas.
Example
• all isomorphic Σ-structures are elementarily equivalent
• (Q, ≤) and (R, ≤) are elementarily equivalent
• (Z, ≤) and (Q, ≤) are not elementarily equivalent
8 / 39
Combined theory: model-based view
T1 ⊕ T2 = {A | A is a Σ-structure,
Σ1-reduct of A is elementarily equivalent to some A1 ∈ T1, and
Σ2-reduct of A is elementarily equivalent to some A2 ∈ T2}
9 / 39
Nelson-Oppen method (1979)
Convention
Without loss of generality, we will consider
only combination of two theories T1 and T2.
10 / 39
Necessary terminology
• i-term = its topmost function symbol is in Σi
• i-atom = its predicate function symbol is in Σi or is of form s = t with i-terms
s and t
• i-literal = i-atom or its negation
• i-pure subformula or subterm = all its function and predicate symbols are
from Σi
• pure subformula or subterm = i-pure for some i
• alien subterm = maximal i-subterm of an atom that is not i-atom
11 / 39
Terminology: examples
f(x + 1) = f(42) ∧ f(g(x)) = x + y ∧ y ≥ x + 10
What are
• LIA-terms, UF-terms?
• LIA-literals, UF-literals?
• pure LIA subterms/subformulas, pure UF subterms/subformulas?
• alien subterms?
12 / 39
Purification
Purification
• given φ, compute φ1 and φ2 such that
– φ1 is 1-pure,
– φ2 is 2-pure, and
– φ1 ∧ φ2 is equisatisfiable with φ
13 / 39
Purification
Purification
• given φ, compute φ1 and φ2 such that
– φ1 is 1-pure,
– φ2 is 2-pure, and
– φ1 ∧ φ2 is equisatisfiable with φ
Algorithm
1. while φ contains any alien subterm t, create a new variable xt, replace all
occurrences of t by xt and add a new equality xt = t
2. now all literals are pure
3. set φi to all i-pure literals
13 / 39
Example
(f(x + 1) = f(42)) ∧ (f(g(x)) = x + y) ∧ (y ≥ x + 10)
14 / 39
Example
(f(x + 1) = f(42)) ∧ (f(g(x)) = x + y) ∧ (y ≥ x + 10)
(f(z) = f(v)) ∧ (w = x + y) ∧ (y ≥ x + 10) ∧ (z = x + 1) ∧ (v = 42) ∧ (w = f(g(x)))
14 / 39
Example
(f(x + 1) = f(42)) ∧ (f(g(x)) = x + y) ∧ (y ≥ x + 10)
(f(z) = f(v)) ∧ (w = x + y) ∧ (y ≥ x + 10) ∧ (z = x + 1) ∧ (v = 42) ∧ (w = f(g(x)))
φ1 = f(z) = f(x) ∧ w = f(g(x))
φ2 = v = x + y ∧ y ≥ x + 10 ∧ w = x + 1 ∧ v = 42
14 / 39
Setup
From now on
• φ = φ1 ∧ φ2
• φ1 is 1-pure
• φ2 is 2-pure
15 / 39
Non-theorem 1
Theorem (Attempt 1)
The following are equivalent
1. φ is (T1 ⊕ T2)-satisfiable
2. φ1 is T1-satisfiable and φ2 is T2-satisfiable.
Does not hold
16 / 39
Non-theorem 1
Theorem (Attempt 1)
The following are equivalent
1. φ is (T1 ⊕ T2)-satisfiable
2. φ1 is T1-satisfiable and φ2 is T2-satisfiable.
Does not hold
• φ1 = (z = x + y) ∧ (v = y + x) is satisfiable in LRA
• φ2 = f(z) ̸= f(v) is satisfiable in UF
• φ = φ1 ∧ φ2 is not satisfiable in LRA ⊕ UF
16 / 39
Interface equalities
Observation
• the T1-model and the T2-model have to agree on interface equalities =
equalities between variables that are shared by φ1 and φ2
Arrangement
• an equivalence R over a finite set of terms S
• induces a formula
arR(S) =
(s,t)∈R
(s = t) ∧
(s,t)̸∈R
(s ̸= t)
• we will consider arrangements over shared variables
C = Vars(φ1) ∩ Vars(φ2).
17 / 39
Non-theorem 2
Theorem (Attempt 2)
The following are equivalent
1. φ is (T1 ⊕ T2)-satisfiable,
2. there is an arrangement R of variables C such that φ1 ∧ arR(C) is
T1-satisfiable and φ2 ∧ arR(C) is T2-satisfiable.
Does not hold
• x = 42 ∧ y = 42 ∧ x = y is satisfiable in LIA
• x = y is satisfiable in BV8 (bit-vectors of width 8)
• x = 42 ∧ y = 42 ∧ x = y is not satisfiable in LIA ⊕ BV8 (why?)
• LIA ⊕ BV8 is empty
18 / 39
Stably infinite theories
Stably infinite theory T
• if φ has a T-model, then it has a T-model with infinite universe
Example
• LIA, LRA, NIA, NRA are stably infinite
• UF is stably infinite
• bit-vectors of fixed width are not stably infinite
• strings of bounded length are not stably infinite
19 / 39
Main theorem
Theorem (Nelson-Oppen, 1980)
If T1 and T2 are stably infinite, then the following are equivalent
1. φ is (T1 ⊕ T2)-satisfiable,
2. there is an arrangement R of variables C such that φ1 ∧ arR(C) is
T1-satisfiable and φ2 ∧ arR(C) is T2-satisfiable.
20 / 39
Main theorem
Theorem (Nelson-Oppen, 1980)
If T1 and T2 are stably infinite, then the following are equivalent
1. φ is (T1 ⊕ T2)-satisfiable,
2. there is an arrangement R of variables C such that φ1 ∧ arR(C) is
T1-satisfiable and φ2 ∧ arR(C) is T2-satisfiable.
Proof (sketch).
• 1 ⇒ 2: straighforward.
• 2 ⇒ 1: get two models A1 and A2; use stable infiniteness and upward
Löwenheim-Skolem theorem to get elementarily equivalent models A′
1 and
A′
2 that have the same cardinality; combine the structures
20 / 39
Non-deterministic Nelson-Oppen algorithm
Algorithm
1. Purify the input formula into φ1 ∧ φ2
2. Non-deterministically guess an arrangement R of shared variables C.
3. Check T1-satisfiability of φ1 ∧ arR(C) and T2 satisfiability of φ2 ∧ arR(C).
4. If both are satisfiable, return satisfiable.
5. Otherwise return unsatisfiable.
21 / 39
Example
φLIA = (v1 ≥ 0) ∧ (v1 ≤ 1) ∧ (v2 = 0) ∧ (v3 = 1)
φUF = (f(v1) ̸= f(v2))
22 / 39
Non-deterministic Nelson-Oppen algorithm
Problems
• non-deterministic algorithms are not practical
• if made deterministic, the number of arrangements is exponential with
respect to |C| (Bell number)
23 / 39
Deterministic Nelson-Oppen algorithm
Idea
• do not guess the arrangement, let the T-solvers build it together
• T1-solver propagates all implied interface equalities (equalities between of
shared variables) to T2-solver
• T2-solver propagates all implied interface equalities to T1-solver
• if both solvers Ti decide that the formulas φi are satisfiable and do not imply
any new equalities, the formula φ is satisfiable
24 / 39
Deterministic Nelson-Oppen algorithm
T1-solver T2-solver
unsat unsat
ci = cj
ci = cj
25 / 39
Deterministic Nelson-Oppen algorithm
Problem
• Does not work in general
26 / 39
Deterministic Nelson-Oppen algorithm
Problem
• Does not work in general
φLIA = (v1 ≥ 0) ∧ (v1 ≤ 1) ∧ (v2 = 0) ∧ (v3 = 1)
φUF = (f(v1) ̸= f(v2)) ∧ (f(v1) ̸= f(v3))
26 / 39
Convexity
Convex theory
• if φ |=T ψ ∨ ρ
• then φ |=T ψ or φ |=T ρ
Example
• UF, LRA are convex
• LIA is not convex:
– x ≥ 1 ∧ x ≤ 2 |=LIA x = 1 ∨ x = 2;
– x ≥ 1 ∧ x ≤ 2 ̸|=LIA x = 1
– x ≥ 1 ∧ x ≤ 2 ̸|=LIA x = 2
27 / 39
Deterministic Nelson-Oppen algorithm
Algorithm
1. Purify the input formula into φ1 ∧ φ2
2. For both i ∈ {1, 2}
2.1 Check satisfiability of φi by Ti
2.2 Detect all equalities of variables C implied by φi
2.3 Propagate them to the Tj solver (i ̸= j)
3. If any of the Ti-solvers returned unsat, return unsat.
4. If no more equalities are propagated, return sat.
5. Go to 2.
Sound and complete for stably infinite and convex theories.
28 / 39
Problems
• deterministic Nelson-Oppen algorithm works only for convex theories
• complete propagation of equalities can be expensive and complicate the
T-solver
29 / 39
Delayed theory combination (2005)
Delayed theory combination
Idea
• combine CDCL(T) and non-determinisic Nelson-Oppen algorithm
• use a SAT solver to “guess” the interface equalities and send them to the
Ti-solvers
• Ti-unsatisfiability causes backtracking in the SAT solver → try another
arrangement
30 / 39
Delayed theory Combination
SAT solver
over Atoms(φ1), Atoms(φ2), and eq = {ci = cj | ci, cj ∈ C, i < j}
T1-solver T2-solver
µAtoms(φ1) µAtoms(φ2)
µeq
sat/unsat sat/unsat
31 / 39
Delayed theory combination
Benefits
• fits well into CDCL(T) paradigm
• the Ti solvers can additionally perform theory propagation (but do not have
to)
32 / 39
Example
φLIA = (v1 ≥ 0) ∧ (v1 ≤ 1) ∧ (v2 = 0) ∧ (v3 = 1)
φUF = (f(v1) ̸= f(v2))
33 / 39
Model-based theory combination (2007)
Problem
• delayed theory combination adds O(|C|2) atoms to the SAT solver
• can slowdown the search
Solution
• be lazy
34 / 39
Model-based theory combination
Algorithm
1. Start DTC with empty set of interface equalities.
2. If unsatisfiable, return unsatisfiable.
3. If satisfiable, check whether the obtained models A1 and A2 agree on all
interface equalities.
3.1 if they do, return satisfiable
3.2 if they do not and all the interface equalities have been added, return
unsatisfiable
3.3 otherwise add the equalities in which they differ to the DTC solver and repeat
35 / 39
Summary of requirements
Non-deterministic Nelson-Oppen
• stably infinite theories
Deterministic Nelson-Oppen
• stably infinite theories
• Ti solvers that can deduce all implied equalities
• convex theories (or deduce also all disjunctions of equalities)
Delayed Theory Combination (and Model-based TC)
• stably infinite theories
36 / 39
Where are we?
Contents
Propositional satisfiability (SAT)
• (A ∨ ¬B) ∧ (¬A ∨ C)
• is it satisfiable?
Satisfiability modulo theories (SMT)
• x = 1 ∧ x = y + y ∧ y > 0
• is it satisfiable over reals?
• is it satisfiable over integers?
• ← YOU ARE STANDING HERE
Automated theorem proving (ATP)
• axioms: ∀x (x + x = 0), ∀x∀y (x + y = y + x)
• do they imply ∀x∀y ((x + y) + (y + x) = 0)? 37 / 39
We already know
• definition of first-order logic
• definition of first-order theories and satisfiability modulo theories
• theories useful in practice
• CDCL(T) algorithm for solving SMT
• several algorithms for T-solvers (UF, difference logic) and ideas of others
• combination of theories
38 / 39
Next time
• satisfiability of quantified formulas
• first-order resolution (again)
• first-order superposition (again)
39 / 39