Out line Propositional Satisfiability Propositional Clauses Backtrack search Unit Propagation DPLL: Unit Propagation Backtrack Search Characteristics of dPLl local search using GSAT 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 or b S C2: Not C or A F C3: Not b or c s3/19/2003 copyright Brian Williams 7 Outline • Propositional Satisfiability • • Backtrack Search • Unit Propagation • DPLL: Unit Propagation + Backtrack Search • Characteristics of DPLL • local search using GSAT 3/19/2003 copyright Brian Williams 8 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 S S S Propositional Clauses