Out line Propositional Satisfiability Propositional Clauses Backtrack search Unit Propagation DPLL: Unit Propagation Backtrack Search Characteristics of dPLl local search using GSAT Propositional Clauses Variables: Propositions Domain True, False] Constraints: Clauses that must be true Clause (not A or B or E) A disjunction of Literals Literal Proposition or its negation Positive Literal Negative Literal Not A3/19/2003 copyright Brian Williams 3 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 4 • Variables: • Domain: • Constraints: Clauses that must be true • Clause (not A or B or E) • A disjunction of Literals • Literal: Proposition or its negation • B • Negative Literal Propositional Clauses Propositional Clauses Propositions Positive Literal Not A {True, False}