10.3.6 Satisfiability

A propositional variable is one that can be assigned the value true or false. A literal is a propositional variable or its negation. A clause is a sequence of literals separated by the logical OR operator. A propositional formula is said to be in conjunctive normal form (CNF) if it consists of a sequence of clauses separated by the logical AND operator. For example,

(p$\vee$  q$\vee$  s)$\wedge$ ($\overline{q}$$\vee$  r)$\wedge$($\overline{p}$$\vee$$\overline{q}$$\vee$  r$\vee$$\overline{s}$)

A truth assignment for a set of propositional variables is an assignment of true or false value to each propositional variable. A truth assignment is said to satisfy a formula if it makes the value of the formula true.

3-SAT (Decision Problem): Given a CNF formula in which each clause is permitted to contain at most three literals, is there a truth assignment to its variables that satisfies it?