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
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
Unit Propagation Idea: Forward checking on binary clauses (not a or B) {T,F}? T, FI Unit propagation If all literals are false, save i then assign true to l (not a( not B(A or B or C) Unit Propagation Examples C1: Not A or B Satisfied C2: Not c or a Satisfied C 3 Not B orC Satisfied C4: A Satisfied C4 CI rue B
3/19/2003 copyright Brian Williams 17 Unit Propagation Idea: Forward checking on binary clauses (not A or B) {F} {T,F} ? {T} {T,F} ? Unit propagation: If all literals are false, save l then assign true to l: • (not A) (not B) (A or B or C) C 3/19/2003 copyright Brian Williams 18 Unit Propagation Examples • C1: Not A or B • C2: Not C or A • C3: Not B or C • C4: A C4 A True C1 B True C3 C True Satisfied Satisfied Satisfied Satisfied
Unit Propagation Examples C1: Not Aor B Satisfied C2: Not CorASatisfied C3 Not b orc Satisfied C4:A C4 rue True True C1 A B C4: Not B Satisfied False False CI B Unit Propagation true fal C2:pV”t CI:TVaVp p procedure propagate( c) ∥ C is a clause if all literals in C are false except I, and I is unassigned then assign true to l and record c as a support for I and or each clause C' mentioning"not I propagate(c) end propagate
3/19/2003 copyright Brian Williams 19 Unit Propagation Examples • C1: Not A or B • C2: Not C or A • C3: Not B or C • C4: A • C4’: Not B C4 C1 C3 C1 C2 C4’ A True B True C True A False B False C False C4 A True Satisfied Satisfied Satisfied Satisfied 3/19/2003 copyright Brian Williams 20 C1 : ¬r q p C2: ¬ p ¬ t r true q false p t procedure propagate(C) // C is a clause if all literals in C are false except l, and l is unassigned then assign true to l and record C as a support for l and for each clause C’ mentioning “not l”, propagate(C’) end propagate Unit Propagation
