Advanced Features of SAT Solvers
IA085: Satisfiability and Automated Reasoning
Martin Jonáš
FI MUNI, Spring 2024
Last Time
• Conflict-Driven Clause Learning (CDCL): DPLL + clause learning + backjumping
• literal decision heuristics
• restarts
1 / 38
Incremental SAT solving
Normal Usage
1. Call solve(Φ).
2. Get the answer (+ possibly a model).
3. ???
4. Profit.
2 / 38
Incremental Usage
Some applications issue incremental queries:
1. Is Φ1 satisfiable?
2. Is Φ1 ∪ Φ2 satisfiable?
3. Is Φ1 ∪ Φ2 ∪ Φ3 satisfiable?
4. . . .
Examples
• symbolic execution
• planning
3 / 38
Incremental Usage
Modern solvers support incremental interface:
1. Add clauses Φ1.
2. Call solve().
3. Do something with the answer.
4. Add clauses Φ2.
5. Call solve().
6. Do something with the answer.
7. Add clauses Φ3.
8. . . .
Why is this better than calling solve for Φ1, for Φ1 ∪ Φ2, for Φ1 ∪ Φ2 ∪ Φ3, . . .?
4 / 38
Solving Under Assumptions
What if we need to solve multiple queries that are not incremental, but differ in
some literals?
• Is Φ ∧ A satisfiable?
• Is Φ ∧ ¬A ∧ B satisfiable?
• Is Φ ∧ ¬B ∧ D ∧ E satisfiable?
• . . .
Examples
• planning (common constraints + individual goals)
• package dependencies (common constraints + individual queries for
installed packages)
5 / 38
Solving Under Assumptions
Solving under assumptions (MiniSAT)
• Add clauses Φ.
• Call solve([A]) and do something with the result.
• Call solve([¬A, B]) and do something with the result.
• Call solve([¬B, D, E]) and do something with the result.
• . . .
The calls to solve() reuse the learnt clauses!
6 / 38
Solving Under Assumptions (alternative API)
Solving under assumptions (CaDiCaL)
• Add clauses Φ.
• Call assume(A).
• Call solve() and do something with the result.
• Call assume(¬A) and assume(B).
• Call solve() and do something with the result.
• Call assume(¬B) and assume(D) and assume(E).
• Call solve() and do something with the result.
• . . .
7 / 38
Solving Under Assumptions: Implementation
solve([l1, l2, ..., lk])
• before the search, decide l1, l2, . . ., lk on dummy decision levels before
decisions level 0
• when backjumping before the real decision level 0, return UNSAT
Nice bonus
• when UNSAT, a slight modification of clause learning (last UIP) can compute a
conflict clause C = ¬µ with µ ⊆ {l1, l2, . . . , lk}
• identifies failed assumptions that contributed to the unsatisfiability
8 / 38
Varying Clauses
What if we need to vary additional clauses, not only literals?
• Is Φ ∧ C1 satisfiable?
• Is Φ ∧ C2 ∧ C3 satisfiable?
• Is Φ ∧ C4 satisfiable?
• . . .
9 / 38
Activation Literals
Solution
• add a new activation literal to each clause that should be possible to disable
Φ ∧ C2 ∧ C3 Φ ∧ (¬A2 ∨ C2) ∧ (¬A3 ∨ C3)
• use solving under assumptions to enable clauses
– solve([¬A2,¬A3]) ≡ is Φ sat?
– solve([ A2,¬A3]) ≡ is Φ ∧ C2 sat?
– solve([¬A2, A3]) ≡ is Φ ∧ C3 sat?
– solve([ A2, A3]) ≡ is Φ ∧ C2 ∧ C3 sat?
10 / 38
Proof generation
Proof Generation
Facts
• SAT solvers are used in safety-critical systems
• SAT solvers are pieces of software
• all software has bugs
11 / 38
Proof Generation
Facts
• SAT solvers are used in safety-critical systems
• SAT solvers are pieces of software
• all software has bugs
•
11 / 38
Proof Generation
Facts
• SAT solvers are used in safety-critical systems
• SAT solvers are pieces of software
• all software has bugs
•
Solution
• besides SAT/UNSAT answer, produce an artifact that can be independently
checked
• for SAT results = model
• for UNSAT results = unsatisfiability proof
11 / 38
Resolution Proof Generation from DPLL
Recall
Each UNSAT run of DPLL corresponds to a tree resolution proof of unsatisfiability
Algorithm
• conflicting clauses (leaves) input clauses
• unit propagation steps resolution with the clause that triggered the unit
propagation
• decision nodes resolution steps on the decided variable
12 / 38
Resolution Proof Generation from DPLL: Example
{{A, B}1, {¬B, C}2, {¬B, ¬C}3, {¬A, ¬B, ¬D}4, {¬A, B, ¬D}5, {¬A, B, D}6}
[]
[A] [¬A]
[A, B] [A, ¬B] [¬A, B]
[A, B, C] [A, ¬B, ¬D] [¬A, B, C]
A
B
C
¬B
¬D
¬A
B
C
13 / 38
Resolution Proof Generation from DPLL: Example
{{A, B}1, {¬B, C}2, {¬B, ¬C}3, {¬A, ¬B, ¬D}4, {¬A, B, ¬D}5, {¬A, B, D}6}
[]
[A] [¬A]
[A, B] [A, ¬B] [¬A, B]
[A, B, C] [A, ¬B, ¬D] [¬A, B, C]
A
B
C
¬B
¬D
¬A
B
C
∅
{A} {A}
{¬B} {¬A, B} {¬B}{A, B}
{¬B, ¬C}{¬B, C} {¬A, B, D}{¬A, B, ¬D} {¬B, ¬C}{¬B, C}
A
B
C
¬B
¬D
¬A
B
C
13 / 38
Resolution Proof Generation from CDCL
CDCL observations
• the final conflict was achieved by backtracked literals and unit propagated
literals (no decisions, why?)
• the final conflict is derived by unit propagation from input clauses and learnt
clauses
• the final conflict can be obtained by resolving input clauses and learnt
clauses
• each learnt clause was obtained by resolving input clauses and previous
learnt clauses
14 / 38
Resolution Proof Generation from CDCL
Algorithm
1. express the final conflict as resolution of input clauses and learnt clauses
2. while the proof contains a leaf that is a learnt clause, replace it by its
resolution proof
Practical considerations
• the solver needs to remember for each learnt clause its antecedent clauses
from which it was obtained
• might require significant amount of memory and makes the solver more
complex
15 / 38
Clausal Proofs
For easier implementation: clausal proofs
• proof is a list of clauses
• each clause has to be entailed by some previous clauses (input or derived)
• SAT solver only outputs the learnt clauses during the search
• proof checker checks the entailment
• examples: DRUP, DRAT
16 / 38
Clausal Proof Formats
{{A, B}1, {¬B, C}2, {¬B, ¬C}3, {¬A, ¬B, ¬D}4, {¬A, B, ¬D}5, {¬A, B, D}6}
DIMACS formula
p cnf 4 6
1 2 0
-2 3 0
-2 -3 0
-1 -2 -4 0
-1 2 -4 0
-1 2 4 0
Clausal proof
-2 0
1 0
-1 2 0
-1 0
0
17 / 38
Reverse Unit Propagation (RUP)
Φ |= (l1 ∨ l2 ∨ . . . ∨ ln) ⇐⇒ Φ ∧ ¬l1 ∧ ¬l2 ∧ . . . ∧ ¬ln |= ⊥
To check clause C = {l1, l2, . . . , ln} using reverse unit propagation (RUP)
1. assign ¬l1, ¬l2, . . . , ¬ln
2. check that unit propagation produces a conflict
Reverse Unit Propagation
• obviously not complete
• sufficient for clauses learnt by CDCL, because it learns clauses that were
conflicting by unit propagation
• previous example was RUP proof
18 / 38
Delete Reverse Unit Propagation (DRUP)
• proof checking of RUP requires checking large number of clauses
• some were actually deleted by the solver and are not needed for the proof
anymore → express deleting (D) in the proof (DRUP)
DIMACS formula
p cnf 4 6
1 2 0
-2 3 0
-2 -3 0
-1 -2 -4 0
-1 2 -4 0
-1 2 4 0
Clausal proof
-2 0
d -2 3 0
d -2 -3 0
1 0
-1 2 0
-1 0
0
19 / 38
Clausal Proof Formats
Multiple clausal proof formats exist besides DRUP
• DRAT
• LRAT
• LPR
• . . .
Most of them have efficient proof checkers (some even formally verified).
20 / 38
Clausal Proof Formats
Multiple clausal proof formats exist besides DRUP
• DRAT
• LRAT
• LPR
• . . .
Most of them have efficient proof checkers (some even formally verified).
Challenge
• implement (D)RUP proof generation in your solver
• use e.g. DRAT-TRIM for proof checking
(https://www.cs.utexas.edu/~marijn/drat-trim/)
20 / 38
Unsatisfiable Cores
Unsatisfiable Cores
Definition
For an unsatisfiable formula Φ in CNF, its subset of clauses Ψ ⊆ Φ is called
unsatisfiable core if Ψ is unsatisfiable.
Important
The set Ψ does not have to be minimal.
Applications
• analysis of requirements
• package dependencies
• abstraction refinement
21 / 38
Unsatisfiable Cores: Proof-based Algorithm
Proof-based algorithm
1. Compute a resolution proof of unsatisfiability of Φ.
2. Return the set Ψ ⊆ Φ of clauses that occur as leaves in the proof.
22 / 38
Unsatisfiable Cores: Proof-based Algorithm
{{A, B}, {D, ¬E}, {¬B, C}, {¬B, ¬C}, {B, ¬E, F}, {¬A, ¬B, ¬D},
{¬A, ¬F}, {¬A, B, ¬D}, {¬E, ¬F}, {¬A, B, D}}
23 / 38
Unsatisfiable Cores: Proof-based Algorithm
{{A, B}, {D, ¬E}, {¬B, C}, {¬B, ¬C}, {B, ¬E, F}, {¬A, ¬B, ¬D},
{¬A, ¬F}, {¬A, B, ¬D}, {¬E, ¬F}, {¬A, B, D}}
{¬B, C} {¬B, ¬C}
{¬B}
{A, B} {¬A, B, ¬D} {¬A, B, D}
{¬A, B}
{A} {¬A}
∅
23 / 38
Unsatisfiable Cores: Proof-based Algorithm
{{A, B}, {D, ¬E}, {¬B, C}, {¬B, ¬C}, {B, ¬E, F}, {¬A, ¬B, ¬D},
{¬A, ¬F}, {¬A, B, ¬D}, {¬E, ¬F}, {¬A, B, D}}
{¬B, C} {¬B, ¬C}
{¬B}
{A, B} {¬A, B, ¬D} {¬A, B, D}
{¬A, B}
{A} {¬A}
∅
23 / 38
Unsatisfiable Cores: Assumption-based Algorithm
Assumption-based algorithm
1. Add a new activation literal ¬Ai to each clause Ci of Φ.
2. Solve under assumptions solve([A1, A2, . . . , A|Φ|]).
3. The result will be UNSAT.
4. The set F ⊆ {A1, A2, . . . , A|Φ|} of failed assumption literals corresponds to an
unsatisfiable core of Φ.
24 / 38
Unsatisfiable Cores: Assumption-based Algorithm
{{A, B},
{D, ¬E},
{¬B, C},
{¬B, ¬C},
{B, ¬E, F},
{¬A, ¬B, ¬D},
{¬A, ¬F},
{¬A, B, ¬D},
{¬E, ¬F},
{¬A, B, D}}
25 / 38
Unsatisfiable Cores: Assumption-based Algorithm
{{A, B},
{D, ¬E},
{¬B, C},
{¬B, ¬C},
{B, ¬E, F},
{¬A, ¬B, ¬D},
{¬A, ¬F},
{¬A, B, ¬D},
{¬E, ¬F},
{¬A, B, D}}
{{¬A1, A, B},
{¬A2, D, ¬E},
{¬A3, ¬B, C},
{¬A4, ¬B, ¬C},
{¬A5, B, ¬E, F},
{¬A6, ¬A, ¬B, ¬D},
{¬A7, ¬A, ¬F},
{¬A8, ¬A, B, ¬D},
{¬A9, ¬E, ¬F},
{¬A10, ¬A, B, D}}
25 / 38
Unsatisfiable Cores: Assumption-based Algorithm
{{A, B},
{D, ¬E},
{¬B, C},
{¬B, ¬C},
{B, ¬E, F},
{¬A, ¬B, ¬D},
{¬A, ¬F},
{¬A, B, ¬D},
{¬E, ¬F},
{¬A, B, D}}
{{¬A1, A, B},
{¬A2, D, ¬E},
{¬A3, ¬B, C},
{¬A4, ¬B, ¬C},
{¬A5, B, ¬E, F},
{¬A6, ¬A, ¬B, ¬D},
{¬A7, ¬A, ¬F},
{¬A8, ¬A, B, ¬D},
{¬A9, ¬E, ¬F},
{¬A10, ¬A, B, D}}
solve([A1, A2, . . . , A10]) =
25 / 38
Unsatisfiable Cores: Assumption-based Algorithm
{{A, B},
{D, ¬E},
{¬B, C},
{¬B, ¬C},
{B, ¬E, F},
{¬A, ¬B, ¬D},
{¬A, ¬F},
{¬A, B, ¬D},
{¬E, ¬F},
{¬A, B, D}}
{{¬A1, A, B},
{¬A2, D, ¬E},
{¬A3, ¬B, C},
{¬A4, ¬B, ¬C},
{¬A5, B, ¬E, F},
{¬A6, ¬A, ¬B, ¬D},
{¬A7, ¬A, ¬F},
{¬A8, ¬A, B, ¬D},
{¬A9, ¬E, ¬F},
{¬A10, ¬A, B, D}}
solve([A1, A2, . . . , A10]) = UNSAT
25 / 38
Unsatisfiable Cores: Assumption-based Algorithm
{{A, B},
{D, ¬E},
{¬B, C},
{¬B, ¬C},
{B, ¬E, F},
{¬A, ¬B, ¬D},
{¬A, ¬F},
{¬A, B, ¬D},
{¬E, ¬F},
{¬A, B, D}}
{{¬A1, A, B},
{¬A2, D, ¬E},
{¬A3, ¬B, C},
{¬A4, ¬B, ¬C},
{¬A5, B, ¬E, F},
{¬A6, ¬A, ¬B, ¬D},
{¬A7, ¬A, ¬F},
{¬A8, ¬A, B, ¬D},
{¬A9, ¬E, ¬F},
{¬A10, ¬A, B, D}}
solve([A1, A2, . . . , A10]) = UNSAT
failed literals {A1, A3, A4, A8, A10}
25 / 38
Unsatisfiable Cores: Assumption-based Algorithm
{{A, B},
{D, ¬E},
{¬B, C},
{¬B, ¬C},
{B, ¬E, F},
{¬A, ¬B, ¬D},
{¬A, ¬F},
{¬A, B, ¬D},
{¬E, ¬F},
{¬A, B, D}}
{{¬A1, A, B},
{¬A2, D, ¬E},
{¬A3, ¬B, C},
{¬A4, ¬B, ¬C},
{¬A5, B, ¬E, F},
{¬A6, ¬A, ¬B, ¬D},
{¬A7, ¬A, ¬F},
{¬A8, ¬A, B, ¬D},
{¬A9, ¬E, ¬F},
{¬A10, ¬A, B, D}}
solve([A1, A2, . . . , A10]) = UNSAT
failed literals {A1, A3, A4, A8, A10}
25 / 38
Interpolation
Craig Interpolants
Definition (Craig Interpolant, 1957)
Given a pair of formulas (A, B) such that A ∧ B |= ⊥, a Craig interpolant is a
formula I such that
• A |= I
• B ∧ I |= ⊥
• Atoms(I) ⊆ Atoms(A) ∩ Atoms(B)
This is the definition used in formal methods, sometimes called reverse Craig
interpolant.
26 / 38
Craig Interpolants: Examples
A = A1 ∧ (¬A1 ∨ C1) ∧ A2 ∧ (¬A2 ∨ C2) ∧ C3
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ C3
27 / 38
Craig Interpolants: Examples
A = A1 ∧ (¬A1 ∨ C1) ∧ A2 ∧ (¬A2 ∨ C2) ∧ C3
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ C3
I = C1 ∧ C2
27 / 38
Craig Interpolants: Examples
A = A1 ∧ (¬A1 ∨ C1) ∧ A2 ∧ (¬A2 ∨ C2) ∧ C3
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ C3
I = C1 ∧ C2
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
27 / 38
Craig Interpolants: Examples
A = A1 ∧ (¬A1 ∨ C1) ∧ A2 ∧ (¬A2 ∨ C2) ∧ C3
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ C3
I = C1 ∧ C2
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
I = (C1 ∨ C3) ∧ (C2 ∨ C3)
27 / 38
Craig Interpolants (alternative definition)
Definition (Craig Interpolant: alternative)
Given a pair of formulas (A, B) such that A |= B, a Craig interpolant is a formula I
such that
• A |= I
• I |= B
• Atoms(I) ⊆ Atoms(A) ∩ Atoms(B)
The definitions are dual: (A, B) is a reverse Craig interpolant iff (A, ¬B) is a Craig
interpolant in the above sense.
We discuss only reverse Craig interpolants from now on.
28 / 38
Craig Interpolation: Usage
Interpolants widely used in formal verification
• overapproximation of image
• computation of function summaries
• generalization of spurious counterexamples
• refinement of predicate abstraction
• . . .
29 / 38
Craig Interpolation: Existence and Size
Theorem (McMillan, 2003)
For every pair of propositional formulas (A, B) such that A ∧ B |= ⊥, a Craig
interpolant can be computed in linear time with respect to the size of a resolution
proof of unsatisfiability of A ∧ B.
30 / 38
Craig Interpolation: Existence and Size
Theorem (McMillan, 2003)
For every pair of propositional formulas (A, B) such that A ∧ B |= ⊥, a Craig
interpolant can be computed in linear time with respect to the size of a resolution
proof of unsatisfiability of A ∧ B.
What does it say about the size of interpolant?
30 / 38
Craig Interpolation: Existence and Size
Theorem (McMillan, 2003)
For every pair of propositional formulas (A, B) such that A ∧ B |= ⊥, a Craig
interpolant can be computed in linear time with respect to the size of a resolution
proof of unsatisfiability of A ∧ B.
What does it say about the size of interpolant?
What does it say about size with respect to |A| + |B|?
30 / 38
Craig Interpolation: Algorithm
Computing Craig Interpolants
1. Get resolution proof of unsatisfiability of A ∧ B.
2. Label nodes of the proof by preliminary interpolants, starting from leaves.
3. The label of root of the proof is the Craig interpolant of (A, B).
31 / 38
Preliminary Interpolants
Definition
A formula f is a preliminary interpolant of the resolution proof node C (written
c [f]) if
1. A |= f
2. B ∧ f |= C
3. Atoms(C) ⊆ Atoms(A) ∪ Atoms(B)
4. Atoms(f) ⊆ Atoms(A) ∩ (Atoms(B) ∪ Atoms(C))
Preliminary interpolant f of the root C = ⊥ is the real Craig interpolant of (A, B).
32 / 38
Interpolation Algorithm
Leaves
C [C]
C ∈ A
C [⊤]
C ∈ B
where φ l
replaces all l in φ by ⊤ and ¬l by ⊥
33 / 38
Interpolation Algorithm
Leaves
C [C]
C ∈ A
C [⊤]
C ∈ B
Inner nodes
(l ∨ C) [f] (¬l ∨ D) [g]
(C ∨ D) [ ]
var(l) ∈ Atoms(B)
(l ∨ C) [f] (¬l ∨ D) [g]
(C ∨ D) [ ]
var(l) ̸∈ Atoms(B)
where φ l
replaces all l in φ by ⊤ and ¬l by ⊥
33 / 38
Interpolation Algorithm
Leaves
C [C]
C ∈ A
C [⊤]
C ∈ B
Inner nodes
(l ∨ C) [f] (¬l ∨ D) [g]
(C ∨ D) [f ∧ g]
var(l) ∈ Atoms(B)
(l ∨ C) [f] (¬l ∨ D) [g]
(C ∨ D) [ ]
var(l) ̸∈ Atoms(B)
where φ l
replaces all l in φ by ⊤ and ¬l by ⊥
33 / 38
Interpolation Algorithm
Leaves
C [C]
C ∈ A
C [⊤]
C ∈ B
Inner nodes
(l ∨ C) [f] (¬l ∨ D) [g]
(C ∨ D) [f ∧ g]
var(l) ∈ Atoms(B)
(l ∨ C) [f] (¬l ∨ D) [g]
(C ∨ D) [f ¬l
∨ g l
]
var(l) ̸∈ Atoms(B)
where φ l
replaces all l in φ by ⊤ and ¬l by ⊥
33 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 ¬A1 ∨ C1 ∨ C3 A2 ¬A2 ∨ C2 ∨ C3
C1 ∨ C3 C2 ∨ C3¬C3 ¬C3
C1 C2¬C1 ∨ B1 ¬C2 ∨ ¬B1
B1 ¬B1
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 A2 ¬A2 ∨ C2 ∨ C3
C1 ∨ C3 C2 ∨ C3¬C3 ¬C3
C1 C2¬C1 ∨ B1 ¬C2 ∨ ¬B1
B1 ¬B1
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 [¬A1 ∨ C1 ∨ C3] A2 ¬A2 ∨ C2 ∨ C3
C1 ∨ C3 C2 ∨ C3¬C3 ¬C3
C1 C2¬C1 ∨ B1 ¬C2 ∨ ¬B1
B1 ¬B1
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 [¬A1 ∨ C1 ∨ C3] A2 [A2] ¬A2 ∨ C2 ∨ C3
C1 ∨ C3 C2 ∨ C3¬C3 ¬C3
C1 C2¬C1 ∨ B1 ¬C2 ∨ ¬B1
B1 ¬B1
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 [¬A1 ∨ C1 ∨ C3] A2 [A2] ¬A2 ∨ C2 ∨ C3 [¬A2 ∨ C2 ∨ C3]
C1 ∨ C3 C2 ∨ C3¬C3 ¬C3
C1 C2¬C1 ∨ B1 ¬C2 ∨ ¬B1
B1 ¬B1
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 [¬A1 ∨ C1 ∨ C3] A2 [A2] ¬A2 ∨ C2 ∨ C3 [¬A2 ∨ C2 ∨ C3]
C1 ∨ C3 C2 ∨ C3¬C3 [⊤] ¬C3
C1 C2¬C1 ∨ B1 ¬C2 ∨ ¬B1
B1 ¬B1
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 [¬A1 ∨ C1 ∨ C3] A2 [A2] ¬A2 ∨ C2 ∨ C3 [¬A2 ∨ C2 ∨ C3]
C1 ∨ C3 C2 ∨ C3¬C3 [⊤] ¬C3 [⊤]
C1 C2¬C1 ∨ B1 ¬C2 ∨ ¬B1
B1 ¬B1
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 [¬A1 ∨ C1 ∨ C3] A2 [A2] ¬A2 ∨ C2 ∨ C3 [¬A2 ∨ C2 ∨ C3]
C1 ∨ C3 C2 ∨ C3¬C3 [⊤] ¬C3 [⊤]
C1 C2¬C1 ∨ B1 [⊤] ¬C2 ∨ ¬B1
B1 ¬B1
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 [¬A1 ∨ C1 ∨ C3] A2 [A2] ¬A2 ∨ C2 ∨ C3 [¬A2 ∨ C2 ∨ C3]
C1 ∨ C3 C2 ∨ C3¬C3 [⊤] ¬C3 [⊤]
C1 C2¬C1 ∨ B1 [⊤] ¬C2 ∨ ¬B1 [⊤]
B1 ¬B1
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 [¬A1 ∨ C1 ∨ C3] A2 [A2] ¬A2 ∨ C2 ∨ C3 [¬A2 ∨ C2 ∨ C3]
C1 ∨ C3 [C1 ∨ C3] C2 ∨ C3¬C3 [⊤] ¬C3 [⊤]
C1 C2¬C1 ∨ B1 [⊤] ¬C2 ∨ ¬B1 [⊤]
B1 ¬B1
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 [¬A1 ∨ C1 ∨ C3] A2 [A2] ¬A2 ∨ C2 ∨ C3 [¬A2 ∨ C2 ∨ C3]
C1 ∨ C3 [C1 ∨ C3] C2 ∨ C3 [C2 ∨ C3]¬C3 [⊤] ¬C3 [⊤]
C1 C2¬C1 ∨ B1 [⊤] ¬C2 ∨ ¬B1 [⊤]
B1 ¬B1
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 [¬A1 ∨ C1 ∨ C3] A2 [A2] ¬A2 ∨ C2 ∨ C3 [¬A2 ∨ C2 ∨ C3]
C1 ∨ C3 [C1 ∨ C3] C2 ∨ C3 [C2 ∨ C3]¬C3 [⊤] ¬C3 [⊤]
C1 [C1 ∨ C3] C2¬C1 ∨ B1 [⊤] ¬C2 ∨ ¬B1 [⊤]
B1 ¬B1
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 [¬A1 ∨ C1 ∨ C3] A2 [A2] ¬A2 ∨ C2 ∨ C3 [¬A2 ∨ C2 ∨ C3]
C1 ∨ C3 [C1 ∨ C3] C2 ∨ C3 [C2 ∨ C3]¬C3 [⊤] ¬C3 [⊤]
C1 [C1 ∨ C3] C2 [C2 ∨ C3]¬C1 ∨ B1 [⊤] ¬C2 ∨ ¬B1 [⊤]
B1 ¬B1
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 [¬A1 ∨ C1 ∨ C3] A2 [A2] ¬A2 ∨ C2 ∨ C3 [¬A2 ∨ C2 ∨ C3]
C1 ∨ C3 [C1 ∨ C3] C2 ∨ C3 [C2 ∨ C3]¬C3 [⊤] ¬C3 [⊤]
C1 [C1 ∨ C3] C2 [C2 ∨ C3]¬C1 ∨ B1 [⊤] ¬C2 ∨ ¬B1 [⊤]
B1 [C1 ∨ C3] ¬B1
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 [¬A1 ∨ C1 ∨ C3] A2 [A2] ¬A2 ∨ C2 ∨ C3 [¬A2 ∨ C2 ∨ C3]
C1 ∨ C3 [C1 ∨ C3] C2 ∨ C3 [C2 ∨ C3]¬C3 [⊤] ¬C3 [⊤]
C1 [C1 ∨ C3] C2 [C2 ∨ C3]¬C1 ∨ B1 [⊤] ¬C2 ∨ ¬B1 [⊤]
B1 [C1 ∨ C3] ¬B1 [C2 ∨ C3]
⊥
34 / 38
Interpolation Algorithm: Example
A = A1 ∧ (¬A1 ∨ C1 ∨ C3) ∧ A2 ∧ (¬A2 ∨ C2 ∨ C3)
B = (¬C1 ∨ B1) ∧ (¬C2 ∨ ¬B1) ∧ ¬C3
A1 [A1] ¬A1 ∨ C1 ∨ C3 [¬A1 ∨ C1 ∨ C3] A2 [A2] ¬A2 ∨ C2 ∨ C3 [¬A2 ∨ C2 ∨ C3]
C1 ∨ C3 [C1 ∨ C3] C2 ∨ C3 [C2 ∨ C3]¬C3 [⊤] ¬C3 [⊤]
C1 [C1 ∨ C3] C2 [C2 ∨ C3]¬C1 ∨ B1 [⊤] ¬C2 ∨ ¬B1 [⊤]
B1 [C1 ∨ C3] ¬B1 [C2 ∨ C3]
⊥ [(C1 ∨ C3) ∧ (C2 ∨ C3)]
34 / 38
Interpolation Algorithm: Correctness
We can prove that
1. if
C [f] ,
then f is a preliminary interpolant of C
2. if
C [f] D [g]
E [h]
and f is a preliminary interpolant of C
and g is preliminary interpolant of D,
then h is preliminary interpolant of E
35 / 38
Where are we?
Contents
Propositional satisfiability (SAT)
• (A ∨ ¬B) ∧ (¬A ∨ C)
• is it satisfiable?
• ← YOU ARE STANDING HERE
Satisfiability modulo theories (SMT)
• x = 1 ∧ x = y + y ∧ y > 0
• is it satisfiable over reals?
• is it satisfiable over integers?
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)?
36 / 38
We already know
• normal forms of propositional logic (CNF)
• efficient conversions (Tseitin encoding)
• resolution method and Davis-Putnam algorithm
• DPLL
• two watched literal scheme for unit propagation and conflict detection
• CDCL (clause learning and backjumping)
• literal decision heuristics, restarts
• incremental solving, proof generation, unsat core generation, interpolant
generation
37 / 38
Next time
• first-order logic
• first-order theories
• satisfiability modulo theories (SMT)
• theories of interest (integer arithmetic, real arithmetic, uninterpreted
functions, arrays, bit-vectors, . . .)
38 / 38