Propositional Satisfiability using Backtrack Search Assign true or false to an unassigned proposition Backtrack as soon as a clause is violated B Example C1: Not a orb s C2: NotC or V C3: Not b or c 义义X Propositional Satisfiability using Backtrack Search Assign true or false to an unassigned proposition. Backtrack as soon as a clause is violated B B○ Example C1: Not A ol8ˇ C2 Not c or a s F/TF C3: Not b orc s 6XXX
3/19/2003 copyright Brian Williams 11 Propositional Satisfiability using Backtrack Search • Assign true or false to an unassigned proposition. • Backtrack as soon as a clause is violated. Example: • C1: Not A or B • C2: Not C or A • C3: Not B or C A F F B C F T T C F T S S v 3/19/2003 copyright Brian Williams 12 Propositional Satisfiability using Backtrack Search • Assign true or false to an unassigned proposition. • Backtrack as soon as a clause is violated. Example: • C1: Not A or B • C2: Not C or A • C3: Not B or C A F F B C F T T C F T B T C F S S v
Propositional Satisfiability using Backtrack Search Assign true or false to an unassigned proposition Backtrack as soon as a clause is violated B Example C1: Not a orBS C C2 Not C ora s C3: Not B or C V 义义X Propositional Satisfiability using Backtrack Search Assign true or false to an unassigned proposition. Backtrack as soon as a clause is violated B B Example C1: Not A or b S C2 Not c or a s F/TF F/T C 3 Not B or C s 占x×x
3/19/2003 copyright Brian Williams 13 Propositional Satisfiability using Backtrack Search • Assign true or false to an unassigned proposition. • Backtrack as soon as a clause is violated. Example: • C1: Not A or B • C2: Not C or A • C3: Not B or C A F F B C F T T C F T B T C F T C F S S v 3/19/2003 copyright Brian Williams 14 Propositional Satisfiability using Backtrack Search • Assign true or false to an unassigned proposition. • Backtrack as soon as a clause is violated. Example: • C1: Not A or B • C2: Not C or A • C3: Not B or C A F F B C F T T C F T B T C F T C F T S S S
Backtrack Search Procedure BT(phi, A) Input: A cnf theory phi, an assignment a to propositions in pl Output: a decision of whether phi is satisfiable 1. If a clause is violated return (false) 2. Else if all propositions are assigned return(true) 3. Else Q= some unassigned proposition in phi Return(BT(phi, A[Q= True]or BT(phi, A[Q= Falsel Out line Propositional Satisfiability Propositional clauses Backtrack Search Unit Propagation DPLL: Unit Propagation Backtrack Search Characteristics of dpll local search using GSAT
3/19/2003 copyright Brian Williams 15 Backtrack Search Procedure BT(phi,A) Input: A cnf theory phi, an assignment A to propositions in phi Output: A decision of whether phi is satisfiable. 1. If a clause is violated return(false); 2. Else if all propositions are assigned return(true); 3. Else Q = some unassigned proposition in phi; 4. Return (BT(phi, A[Q = True]) or 5. BT(phi, A[Q = False]) 3/19/2003 copyright Brian Williams 16 Outline • Propositional Satisfiability • • Backtrack Search • Unit Propagation • DPLL: Unit Propagation + Backtrack Search • Characteristics of DPLL • local search using GSAT Propositional Clauses