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 folding3/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