Unsatisfiability Proofs
Henrich Lauko
IA072 – Seminar on Concurrency
November 30, 2016
Is SAT solver credible?
Possible results:
SAT
UNSAT
TIMEOUT
1 / 22
Criteria on unsatisfiability proofs
easily checkable
2 / 22
Criteria on unsatisfiability proofs
easily checkable
small/reasonable size
2 / 22
Criteria on unsatisfiability proofs
easily checkable
small/reasonable size
proof checking quicker than solver
2 / 22
Criteria on unsatisfiability proofs
easily checkable
small/reasonable size
proof checking quicker than solver
proof production not slowing down the solver
2 / 22
Criteria on unsatisfiability proofs
easily checkable
small/reasonable size
proof checking quicker than solver
proof production not slowing down the solver
minimize modifications of solver
2 / 22
Resolution
Resolution rule:
x ∨ C ¬x ∨ D
C ∨ D
x
We write (x ∨ C) (¬x ∨ D) = (C ∨ D).
3 / 22
Resolution
Resolution rule:
x ∨ C ¬x ∨ D
C ∨ D
x
We write (x ∨ C) (¬x ∨ D) = (C ∨ D).
Resolution chain
((a ∨ c) (¬a ∨ b)) (¬a ∨ ¬b) = (¬a ∨ c)
Resolution chains are computed from left.
3 / 22
Resolution proofs – TraceCheck proof format
ϕ = (¬b∨c) ∧ (a∨c) ∧ (¬a∨b) ∧ (¬a∨¬b) ∧ (a∨¬b) ∧ (b∨¬c)
4 / 22
Resolution proofs – TraceCheck proof format
ϕ = (¬b∨c) ∧ (a∨c) ∧ (¬a∨b) ∧ (¬a∨¬b) ∧ (a∨¬b) ∧ (b∨¬c)
(¬a ∨ ¬b) (a ∨ ¬b) = ¬b
(a ∨ c) (¬a ∨ b) (¬b ∨ c) = c
(b ∨ ¬c) (¬b) (c) = ∅
4 / 22
Resolution proofs – TraceCheck proof format
ϕ = (¬b∨c) ∧ (a∨c) ∧ (¬a∨b) ∧ (¬a∨¬b) ∧ (a∨¬b) ∧ (b∨¬c)
(¬a ∨ ¬b) (a ∨ ¬b) = ¬b
(a ∨ c) (¬a ∨ b) (¬b ∨ c) = c
(b ∨ ¬c) (¬b) (c) = ∅
1 -2 3 0 0
2 1 3 0 0
3 -1 2 0 0
4 -1 -2 0 0
5 1 -2 0 0
6 2 -3 0 0
7 -2 0 4 5 0
8 3 0 1 2 3 0
9 0 6 7 8 0
4 / 22
Imperfections of resolution proofs
1 -2 3 0 0
2 1 3 0 0
3 -1 2 0 0
4 -1 -2 0 0
5 1 -2 0 0
6 2 -3 0 0
7 -2 0 4 5 0
8 3 0 1 2 3 0
9 0 6 7 8 0
5 / 22
Imperfections of resolution proofs
1 -2 3 0 0
2 1 3 0 0
3 -1 2 0 0
4 -1 -2 0 0
5 1 -2 0 0
6 2 -3 0 0
7 -2 0 4 5 0
8 3 0 1 2 3 0
9 0 6 7 8 0
extremely large (dozens of
gigabytes)
5 / 22
Imperfections of resolution proofs
1 -2 3 0 0
2 1 3 0 0
3 -1 2 0 0
4 -1 -2 0 0
5 1 -2 0 0
6 2 -3 0 0
7 -2 0 4 5 0
8 3 0 1 2 3 0
9 0 6 7 8 0
extremely large (dozens of
gigabytes)
hard to modify solver
5 / 22
Imperfections of resolution proofs
1 -2 3 0 0
2 1 3 0 0
3 -1 2 0 0
4 -1 -2 0 0
5 1 -2 0 0
6 2 -3 0 0
7 -2 0 4 5 0
8 3 0 1 2 3 0
9 0 6 7 8 0
extremely large (dozens of
gigabytes)
hard to modify solver
computationaly hard for
solver to find correct order
of resolutions and determine
the clauses on which to
apply resolution
5 / 22
Imperfections of resolution proofs
1 -2 3 0 0
2 1 3 0 0
3 -1 2 0 0
4 -1 -2 0 0
5 1 -2 0 0
6 2 -3 0 0
7 -2 0 4 5 0
8 3 0 1 2 3 0
9 0 6 7 8 0
extremely large (dozens of
gigabytes)
hard to modify solver
computationaly hard for
solver to find correct order
of resolutions and determine
the clauses on which to
apply resolution
but easy to check – in
deterministic log space
5 / 22
Looking for better proofs
2003 – Goldberg and Novikov introduced Clausal proofs
Clausal proof
Clausal proof P is represented as queue of lemmas l1, . . . , ln, where
ln = ∅.
6 / 22
Looking for better proofs
2003 – Goldberg and Novikov introduced Clausal proofs
Clausal proof
Clausal proof P is represented as queue of lemmas l1, . . . , ln, where
ln = ∅.
We want lemmas to be implied by ϕ, because then
BCP(ϕ ∧ ¬l) produces empty clause ∅.
6 / 22
Reverse unit propagation clause (RUP)
Unit clause and Unit propagation
Given a formula ϕ, if unit propagation on ϕ produces ∅, then
ϕ is unsatisfiable.
7 / 22
Reverse unit propagation clause (RUP)
Unit clause and Unit propagation
Given a formula ϕ, if unit propagation on ϕ produces ∅, then
ϕ is unsatisfiable.
Reverse unit propagation clause
Let C = (l1 ∨ l2 · · · ∨ ln) and ¬C = (¬l1) ∧ (¬l2) ∧ · · · ∧ (¬ln).
Then C is RUP clause with respect to ϕ, if ϕ ∧ ¬C 1 ∅.
Reverse because unit clauses ¬C are propagated back into
earlier clauses.
Typical RUP clauses are the learned clauses in CDCL.
7 / 22
RUP format
RUP proof
Given a fomula ϕ, a clausal proof P = {l1, . . . , ln} is a valid RUP
proof for ϕ if ln = ∅ and for all li holds that:
ϕ ∧ l1 ∧ · · · ∧ li−1 ∧ ¬li 1 ∅
8 / 22
RUP format
RUP proof
Given a fomula ϕ, a clausal proof P = {l1, . . . , ln} is a valid RUP
proof for ϕ if ln = ∅ and for all li holds that:
ϕ ∧ l1 ∧ · · · ∧ li−1 ∧ ¬li 1 ∅
ϕ = (¬b∨c) ∧ (a∨c) ∧ (¬a∨b) ∧ (¬a∨¬b) ∧ (a∨¬b) ∧ (b∨¬c)
Clausal proof (RUP)
-2 0
3 0
0
Pϕ := {(¬b), (c), ∅}
ϕ ∧ (b) 1 ∅
ϕ ∧ (¬b) ∧ (¬c) 1 ∅
ϕ ∧ (¬b) ∧ (c) ∧ (¬∅) 1 ∅
8 / 22
RUP checking
1 RUPchecker(CNF formula ϕ, queue Q of lemmas)
2 while Q is not empty
3 l ← Q.dequeue ()
4 ϕ ← BCP(ϕ ∧ ¬l)
5 if (∅ ∈ ϕ ) then
6 return "checking failed"
7 ϕ ← BCP(ϕ ∧ l)
8 if (∅ ∈ ϕ) then
9 return UNSAT
10 return "all lemmas validated"
1 BCP(CNF formula ϕ)
2 while ∃(x) ∈ ϕ
3 for c ∈ ϕ with ¬x ∈ c
4 c ← c \ {¬x}
5 for c ∈ ϕ with x ∈ c
6 ϕ ← ϕ \ {c}
7 return F
9 / 22
RUP summary
Pros
significantly smaller
minor modifications to solver
Cons
expensive checking
complex algorithms for
checking
10 / 22
RUP summary
Pros
significantly smaller
minor modifications to solver
Cons
expensive checking
complex algorithms for
checking
DRUP – Delete Reverse Unit Propagtion
Format extends RUP by integrating clause deletion information
into proofs.
10 / 22
Generalization of clausal proofs
Clauses in clausal proof are redundant clauses.
11 / 22
Generalization of clausal proofs
Clauses in clausal proof are redundant clauses.
Redundancy properties
1 tautology (T)
11 / 22
Generalization of clausal proofs
Clauses in clausal proof are redundant clauses.
Redundancy properties
1 tautology (T)
2 asymmetric tautology (AT) – if ALA(ϕ, C) has property T
Asymmetric literal addition (ALA)
ALA(ϕ, C) computes C until fixpoint as follows, if l1, . . . , lk ∈ C and there
is a clause (l1 ∨ · · · ∨ lk ∨ l) ∈ ϕ \ {C} for some literal l, let C := C ∨ ¬l.
11 / 22
Generalization of clausal proofs
Clauses in clausal proof are redundant clauses.
Redundancy properties
1 tautology (T)
2 asymmetric tautology (AT) – if ALA(ϕ, C) has property T
3 resolution tautology (RT) = blocked clauses
Asymmetric literal addition (ALA)
ALA(ϕ, C) computes C until fixpoint as follows, if l1, . . . , lk ∈ C and there
is a clause (l1 ∨ · · · ∨ lk ∨ l) ∈ ϕ \ {C} for some literal l, let C := C ∨ ¬l.
Resolution property RP
(i) C has property P or (ii) There is a literal l ∈ ϕ such that for each
clause C ∈ ϕ with ¬l ∈ C , each resolvent C C has P.
11 / 22
Generalization of clausal proofs
Clauses in clausal proof are redundant clauses.
Redundancy properties
1 tautology (T)
2 asymmetric tautology (AT) – if ALA(ϕ, C) has property T
3 resolution tautology (RT) = blocked clauses
4 resolution asymmetric tautology (RAT)
Asymmetric literal addition (ALA)
ALA(ϕ, C) computes C until fixpoint as follows, if l1, . . . , lk ∈ C and there
is a clause (l1 ∨ · · · ∨ lk ∨ l) ∈ ϕ \ {C} for some literal l, let C := C ∨ ¬l.
Resolution property RP
(i) C has property P or (ii) There is a literal l ∈ ϕ such that for each
clause C ∈ ϕ with ¬l ∈ C , each resolvent C C has P.
11 / 22
Example
ϕ = (a ∨ b) ∧ (b ∨ c) ∧ (¬b ∨ ¬c)
(a ∨ ¬a)
12 / 22
Example
ϕ = (a ∨ b) ∧ (b ∨ c) ∧ (¬b ∨ ¬c)
(a ∨ ¬a)
– has T
12 / 22
Example
ϕ = (a ∨ b) ∧ (b ∨ c) ∧ (¬b ∨ ¬c)
(a ∨ ¬a)
– has T
(a ∨ ¬c)
12 / 22
Example
ϕ = (a ∨ b) ∧ (b ∨ c) ∧ (¬b ∨ ¬c)
(a ∨ ¬a)
– has T
(a ∨ ¬c)
– does not have T
12 / 22
Example
ϕ = (a ∨ b) ∧ (b ∨ c) ∧ (¬b ∨ ¬c)
(a ∨ ¬a)
– has T
(a ∨ ¬c)
– does not have T
– has AT because unit propagation under (¬a ∧ c) results in
conflict
12 / 22
Example
ϕ = (a ∨ b) ∧ (b ∨ c) ∧ (¬b ∨ ¬c)
(a ∨ ¬a)
– has T
(a ∨ ¬c)
– does not have T
– has AT because unit propagation under (¬a ∧ c) results in
conflict
– has RT on literal a, because ϕ contains no clauses with ¬a
12 / 22
Example
ϕ = (a ∨ b) ∧ (b ∨ c) ∧ (¬b ∨ ¬c)
(a ∨ ¬a)
– has T
(a ∨ ¬c)
– does not have T
– has AT because unit propagation under (¬a ∧ c) results in
conflict
– has RT on literal a, because ϕ contains no clauses with ¬a
12 / 22
Example
ϕ = (a ∨ b) ∧ (b ∨ c) ∧ (¬b ∨ ¬c)
(a ∨ ¬a)
– has T
(a ∨ ¬c)
– does not have T
– has AT because unit propagation under (¬a ∧ c) results in
conflict
– has RT on literal a, because ϕ contains no clauses with ¬a
(¬a ∨ c)
12 / 22
Example
ϕ = (a ∨ b) ∧ (b ∨ c) ∧ (¬b ∨ ¬c)
(a ∨ ¬a)
– has T
(a ∨ ¬c)
– does not have T
– has AT because unit propagation under (¬a ∧ c) results in
conflict
– has RT on literal a, because ϕ contains no clauses with ¬a
(¬a ∨ c)
– does not have T
12 / 22
Example
ϕ = (a ∨ b) ∧ (b ∨ c) ∧ (¬b ∨ ¬c)
(a ∨ ¬a)
– has T
(a ∨ ¬c)
– does not have T
– has AT because unit propagation under (¬a ∧ c) results in
conflict
– has RT on literal a, because ϕ contains no clauses with ¬a
(¬a ∨ c)
– does not have T
– does not have AT
12 / 22
Example
ϕ = (a ∨ b) ∧ (b ∨ c) ∧ (¬b ∨ ¬c)
(a ∨ ¬a)
– has T
(a ∨ ¬c)
– does not have T
– has AT because unit propagation under (¬a ∧ c) results in
conflict
– has RT on literal a, because ϕ contains no clauses with ¬a
(¬a ∨ c)
– does not have T
– does not have AT
– does not have RT, there is no tautological resolvent on ¬a on
(a ∨ b) and for c on (¬b ∨ ¬c)
12 / 22
Example
ϕ = (a ∨ b) ∧ (b ∨ c) ∧ (¬b ∨ ¬c)
(a ∨ ¬a)
– has T
(a ∨ ¬c)
– does not have T
– has AT because unit propagation under (¬a ∧ c) results in
conflict
– has RT on literal a, because ϕ contains no clauses with ¬a
(¬a ∨ c)
– does not have T
– does not have AT
– does not have RT, there is no tautological resolvent on ¬a on
(a ∨ b) and for c on (¬b ∨ ¬c)
– has RAT, because (¬a ∨ c) (a ∨ b) = (b ∨ c) and unit
propagation on (¬b ∧ ¬c) results in conflict
12 / 22
More redundancy properties
13 / 22
Extended resolution
Extension rule
Allows to iteratively add definitions of form x := a ∧ b by adding
caluses (x ∨ ¬a ∨ ¬b) ∧ (¬x ∨ a) ∧ (¬x ∨ v).
14 / 22
Blocked clauses
Blocked clause
Given formula ϕ, a clause C, and literal l ∈ C, the literal l blocks
C with respect to ϕ if:
1 for each clause D ∈ ϕ with ¬l ∈ D, C l D is tautology, or
2 ¬l ∈ C, i.e., C itself is tautology.
15 / 22
Blocked clauses
Blocked clause
Given formula ϕ, a clause C, and literal l ∈ C, the literal l blocks
C with respect to ϕ if:
1 for each clause D ∈ ϕ with ¬l ∈ D, C l D is tautology, or
2 ¬l ∈ C, i.e., C itself is tautology.
Example
ϕ = (¬b ∨ c) ∧ (a ∨ c) ∧ (¬a ∨ b) ∧ (¬a ∨ ¬b) ∧ (a ∨ ¬b) ∧ (b ∨ ¬c)
(¬b ∨ c) is blocked on c, because (¬b ∨ c) c (b ∨ ¬c) = (¬b ∨ b).
Since ϕ is unsatisfiable, ϕ \ {(¬b ∨ c)} must be unsatisfiable.
15 / 22
Blocked clauses
Blocked clause
Given formula ϕ, a clause C, and literal l ∈ C, the literal l blocks
C with respect to ϕ if:
1 for each clause D ∈ ϕ with ¬l ∈ D, C l D is tautology, or
2 ¬l ∈ C, i.e., C itself is tautology.
Example
ϕ = (¬b ∨ c) ∧ (a ∨ c) ∧ (¬a ∨ b) ∧ (¬a ∨ ¬b) ∧ (a ∨ ¬b) ∧ (b ∨ ¬c)
(¬b ∨ c) is blocked on c, because (¬b ∨ c) c (b ∨ ¬c) = (¬b ∨ b).
Since ϕ is unsatisfiable, ϕ \ {(¬b ∨ c)} must be unsatisfiable.
Blocked clause addition is generalization of extended resolution.
May add clauses not logically implied by the formula.
15 / 22
Resolution Asymmetric Tautologies (RAT)
Resolution asymmetric tautology
Clause C has RAT on l with respect to ϕ if for all D ∈ ϕ with
¬l ∈ D holds that
ϕ ∧ ¬C ∧ (¬D \ (l)) 1 ∅
16 / 22
Resolution Asymmetric Tautologies (RAT)
Resolution asymmetric tautology
Clause C has RAT on l with respect to ϕ if for all D ∈ ϕ with
¬l ∈ D holds that
ϕ ∧ ¬C ∧ (¬D \ (l)) 1 ∅
RAT is generalization of RUP clauses:
ϕ ∧ ¬C 1 ∅ =⇒ ϕ ∧ ¬C ∧ (¬D \ (l)) 1 ∅
16 / 22
Resolution Asymmetric Tautologies (RAT)
Resolution asymmetric tautology
Clause C has RAT on l with respect to ϕ if for all D ∈ ϕ with
¬l ∈ D holds that
ϕ ∧ ¬C ∧ (¬D \ (l)) 1 ∅
RAT is generalization of RUP clauses:
ϕ ∧ ¬C 1 ∅ =⇒ ϕ ∧ ¬C ∧ (¬D \ (l)) 1 ∅
and, if clause C is blocked on l, then for all D ∈ ϕ with ¬l ∈ D
holds that C contains a literal k = l such that ¬k ∈ D, so:
ϕ ∧ (k) ∧ (¬k) 1 ∅ =⇒ ϕ ∧ ¬C ∧ (¬D \ (l)) 1 ∅
16 / 22
Excursion to bounded variable addition
Bounded variable addition
Adds new variable to express dependenties of variables in clauses
and potentially shrinks the formula.
Example
ϕ = (¬a∨¬b∨¬c) ∧ (a∨d) ∧ (a∨e) ∧ (b∨d) ∧ (b∨e) ∧ (c∨d)
BVA introduces a new variable f.
ϕ = (f ∨ a) ∧ (f ∨ b) ∧ (f ∨ c) ∧ (¬f ∨ d) ∧ (¬f ∨ e)
Cannot be expressed only with resolution steps.
17 / 22
Proofs with extended resolution – RAT and DRAT
Extends RUP format with RAT lemmas.
ϕ = (¬a ∨ ¬b ∨ ¬c) ∧ (a ∨ d) ∧
(a ∨ e) ∧ (b ∨ d) ∧ (b ∨ e) ∧
(c ∨ d) ∧ (c ∨ e) ∧ (¬d ∨ ¬e)
Uses BVA to replace first six
clauses by five new cluses using a
fresh new variable
New clauses are RAT clauses.
Final proof is only {(f), ∅}.
6 1 0
6 2 0
6 3 0
-6 4 0
-6 5 0
d 1 4 0
d 2 4 0
d 3 4 0
d 1 5 0
d 2 5 0
d 3 5 0
6 0
0
18 / 22
RAT checking
Resolution asymmetric tautology
Clause C has RAT on l with respect to ϕ if for all D ∈ ϕ with
¬l ∈ D holds that
ϕ ∧ ¬C ∧ (¬D \ (l)) 1 ∅
1 RATchecker(CNF formula ϕ, queue Q of lemmas)
2 while Q is not empty
3 L ← Q.dequeue ()
4 if ∅ ∈ BCP(ϕ ∧ ¬L) then // check if L has AT
5 let l be the first literal in L // L has RAT on l
6 forall C ∈ ϕ¬l do
7 R ← C L
8 if ∅ ∈ BCP(ϕ ∧ ¬R)
9 return "checking failed"
10 ϕ ← BCP(ϕ ∧ L)
11 if ∅ ∈ ϕ
12 return UNSAT
13 return "all lemmas validated"
19 / 22
Some comparison
20 / 22
Benchmarks
21 / 22
Proofs limitations
no method for easy extraction of unsatisfiability proofs from
lookahead solvers
how to handle preprocessing of formulas (Gaussian
Elimination, Cardinality Resolution, Symmetry Breaking)
no common API for proof manipulations
extraction of resolution proof from clausal proof
using clausal proofs for interpolants generation
22 / 22