lecture 7

Views:
 
Category: Entertainment
     
 

Presentation Description

No description available.

Comments

Presentation Transcript

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; } } }

authorStream Live Help