Propositional Logic and Satisfiability Brian c. williams 16.410 October 12003 copyright Bran Williams Reading Assignments: Propositional Logic AIMA Ch 6- Propositional Logic
3/19/2003 copyright Brian Williams 1 and Satisfiability Brian C. Williams 16.410 October 1, 2003 3/19/2003 copyright Brian Williams 2 Reading Assignments: Propositional Logic • Propositional Logic AIMA Ch. 6 – Propositional Logic
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 A
3/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}
Propositional Satisfiability A truth assignment to all propositions such that all clauses are satisfied a clause is satisfied if and only if at least one literal is true a clause is violated if and only if all literals are false (not A or B or E) Propositional Satisfiability Find a truth assignment that satisfies logical sentence T Reduce sentence T to clausal form Perform search similar to Forward Checking Propositional satisfiability testing 1990: 100 variables /200 clauses(constraints) 1998:10,000-100,000vars/10~6 clauses Novel applications e.g. diagnosis, planning, software /circuit testing machine learning, and protein folding
3/19/2003 copyright Brian Williams 5 Propositional Satisfiability • A truth assignment to all propositions such that all clauses are satisfied. • A clause is satisfied if and only if at least one literal is true. • A clause is violated if and only if all literals are false. • (not A or B or E) 3/19/2003 copyright Brian Williams 6 Propositional Satisfiability Propositional Satisfiability Find a truth assignment that satisfies logical sentence T: • Reduce sentence T to clausal form. • Perform search similar to Forward Checking Propositional satisfiability testing: 1990: 100 variables / 200 clauses (constraints) 1998: 10,000 - 100,000 vars / 10^6 clauses Novel applications: e.g. diagnosis, planning, software / circuit testing, machine learning, and protein folding
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 s
3/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
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 Au C3: Not b or c s 义 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 S F/TF C3: Not B or Cv 占义
3/19/2003 copyright Brian Williams 9 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 S u S 3/19/2003 copyright Brian Williams 10 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 S S v