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 GSAT3/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