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