Search in the semantic domain: Search in the semantic domain
Some definitions: Some definitions atomic formula: smallest formula possible (no sub-formulas)
literal: atomic formula or negation of an atomic formula
clause: disjunction of literals
CNF: Conjunction of clauses (A Ç : B Ç C) Æ
(D Ç B Ç E) Æ atomic literal clause
DPLL backtracking search algorithm: DPLL backtracking search algorithm David-Puttnam-Logemann-Loveland
Algorithm: given a formula, return SAT or UNSAT
SAT: there some truth assignment that makes the formula true
UNSAT: formula is false on all truth assignments
Key idea
Pick a literal
Assign literal to true, simplify the formula, and recurse
Assign literal to false, simplify the formula, and recurse
In more detail: In more detail If formula is false, return UNSAT
else If formula is true, return SAT
else:
Pick a literal
Assign literal to true, simplify the formula, and recurse
If recursive call returns SAT, return SAT
Assign literal to false, simplify the formula, and recurse
If recursive call returns SAT, return SAT
If both recursive calls return UNSAT, return UNSAT
Example simplification: Example simplification (A Ç : B Ç C) Æ
(D Ç B Ç E) Æ
(: A Ç D Ç : E) A to true (A Ç : B Ç C) Æ
(D Ç B Ç E) Æ
(: A Ç D Ç : E) (A Ç : B Ç C) Æ
(D Ç B Ç E) Æ
(: A Ç D Ç : E) A to false (A Ç : B Ç C) Æ
(D Ç B Ç E) Æ
(: A Ç D Ç : E)
How do formulas become true or false?: How do formulas become true or false? Formula becomes true
when conjunction becomes empty
Formula becomes false
when clause becomes empty
Search tree: Search tree (A Ç B) Æ
(A Ç : B)
Search tree: Search tree (A Ç B) Æ
(A Ç : B)
Choice of literal matters: Choice of literal matters C Æ
(B Ç : C) Æ
(A Ç : B) Æ
: A
Choice of literal matters: Choice of literal matters C Æ
(B Ç : C) Æ
(A Ç : B) Æ
: A
Choice of literal matters: Choice of literal matters C Æ
(B Ç : C) Æ
(A Ç : B) Æ
: A
Some heuristics for picking literal: Some heuristics for picking literal Pick literals that appear in unit clauses (called unit propagation)
Pick literals that always appear in the same polarity (A or : A) C Æ
(B Ç : C) Æ
(A Ç : B) Æ
: A (A Ç B) Æ
(A Ç : B) Æ
(C Ç B) Æ
(: C Ç : B) Why? Because of the following optimization:
if pick A, don’t explore : A branch
if pick : A, don’t explore A branch
Some heuristics for picking literal: Some heuristics for picking literal Pick literals for which the formula can be expressed as (R Ç A) Æ (Q Ç : A) Æ S
Can then merge both subtrees into just one subtree that checks (R Ç Q) Æ S
These are just a few simple heuristics
Many other heuristics have been developed
Decades of research on this
Extending backtracking search: Extending backtracking search Let’s assume we also have equality with uninterpreted function symbols, for example:
( f(f(a)) = a Ç : (f(a) = f(b)) ) Æ
( a = b Æ f(a) = f(f(b)) )
Some observations
We can still simplify a formula based on a literal being T or F
But we can only simplify that literal
For instance, in the example above, once we’ve assumed a = b, how do we know that : (f(a) = f(b)) is false?
Keep an environment: Keep an environment
Keep an environment: Keep an environment ( f(f(a)) = a Ç : (f(a) = f(b)) ) Æ
( a = b Æ f(a) = f(f(b)) )
Keep an environment: Keep an environment ( f(f(a)) = a Ç : (f(a) = f(b)) ) Æ
( a = b Æ f(a) = f(f(b)) )
Davis-Putnam paper: Davis-Putnam paper Semi-algorithm for first-order logic
Refutation based: negation formula, and show that formula is unsatisfiable
Uses successive SAT instances
Prenex normal form: Prenex normal form Prenex normal form: all quantifiers on the outside
Some example conversions:
9 x.P(x) Æ 9 x. Q(x)
8 x. P(x) Ç 8 x. Q(x)
In general can convert any formula into prenex normal form
Getting rid of existentials: Getting rid of existentials Replace existential with a function symbol that takes as parameters the enclosing universally quantified variables
Transform:
8 x1. 9 x2. 8 x3. 9 x4 R(x1, x2,x3,x4)
Into
8 x1. 8 x3. R(x1, f2(x1),x3,f4(x1, x3))
Herbrand’s universe of a formula: Herbrand’s universe of a formula Given a formula F, we call HF the Herbrand universe of the formula
All constants in F belong to HF (if F does not have constants, then HF includes a fresh constant a)
For any function symbol of arity n occurring in F, and for any t1, …, tn belonging to HF, f(t1, …, tn) also belongs to HF
H_F is the minimal set that satisfies these constraints
Quantifier free lines: Quantifier free lines Instantiate body of a formula F with elements of HF
Suppose F = 8 x1, x2 R(x1, f(x1), x2)
H_F = { a, f(a), f(f(a)), … }
Quantifier free lines:
R(a, f(a), a)
R(a, f(a), f(a))
R(f(a), f(f(a)), a)
… Each line is implied by original formula
As a result, if the conjunction of some quantifier free lines is inconsistent, so is the original formula
Quantifier free lines: Quantifier free lines Each quantifier free line is implied by original formula
As a result, if the conjunction of some quantifier free lines is inconsistent, so is the original formula
If the conjunction of the first n quantifier free lines is consistent, for any n, then the original formula is consistent
Follows from the fact that an infinite sets of quantifier-free formulas is inconsistent iff some finite subset is inconsistent
Example: Example 8 x. : P(x) Ç 9 x. P(x)
Example: Example 8 x. : P(x) Ç 9 x. P(x)
ATP using Lazy Proof Explication: ATP using Lazy Proof Explication a = b Æ (: (f(a) = f(b)) Ç b = c) Æ : (f(a) = f(c))
ATP using Lazy Proof Explication: ATP using Lazy Proof Explication a = b Æ (: (f(a) = f(b)) Ç b = c) Æ : (f(a) = f(c))
Assign proxies:
x1 Æ (: x2 Ç x3) Æ : x4
Use SAT solver: if SAT solver says unsatisfiable, then original formula is unsatisfiable
ATP using Lazy Proof Explication: ATP using Lazy Proof Explication In this case, say SAT solver comes back with x1 set to true, and x2, x3, and x4 set to false
In the propositional world, this is a valid truth assignment
But when considering the underlying meaning of the proxies, we notice that x1 being true and x2 being false is an inconsistency
If the backtracking search is not aware of this, it will continue considering truth assignments with this same inconsistency (for example x1 = x3 = true, x2 = x4 = false)
Key idea: Key idea Have decision procedures return an explicating proof as to why the inconsistency occurred.
The new formula becomes: F Æ proof
The proof reflects the decision procedure’s knowledge back into the propositional world, and can then be used in the prop world to prune the search
In the example, the proof is:
a = b ) f(a) = f(b)
Example continued: Example continued Formula becomes:
x1 Æ (: x2 Ç x3) Æ : x4 Æ (: x1 Ç x2)
Note that SAT solver cannot find the original satisfying assignment (x1 set to true, and x2, x3, and x4 set to false)
Nor can it come back with any assignment that has x1 set to true and x2 set to false
Example continued: Example continued So SAT solver comes back with: x1, x2, x3 set to true, and x4 set to false
This assignment is also inconsistent when considering the underlying meaning of proxies
Explicating proof:
(a = b Æ b = c) ) f(a) = f(c)
Example continued: Example continued New formula:
x1 Æ (: x2 Ç x3) Æ : x4 Æ (: x1 Ç x2) Æ
(: x1 Ç : x3 Ç x4)
SAT solver returns unsatisfiable, and so we know the original formula is unsatisfiable.
Algorithm in more detail: Algorithm in more detail function satisfy(Formula F): Monome {
while (true)
“allocate proxy prop vars for atomic formulas in F, and create
mapping from proxies to atomic formulas”
TruthAssignment A := SAT-solve(-1(F));
if (A = null) { // F is unsatisfiable
return null
} else
Monome M := (A);
Formula E := check(M);
if (E = null) { // M is satisfiable, and so is F
return M;
} else {
F := F Æ E;
}
}
}