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×x3/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