Normal Forms 129Then, Oi is a tautology if and only if Oi contains two literals, )Xa and Xb, where X-a = ')b
and 1 <a A b <im.
Proof. The proofs of parts (a) and (b) just formalize what was done in Example 10. U
2.5.6 The Famous P 5# VAP Conjecture
How easy is it to test whether a formula in DNF is satisfiable or whether a formula in
CNF is a tautology? One way to check whether a CNF formula q5 is satisfiable is to write
its truth table, but this can be a time-consuming process. A formula 4 with n symbols
may contain more than n/4 different proposition letters. The truth table has to have a
row for each assignment of T's and F's to these n/4 proposition letters-thus, 2 n/4 rows.
Hence, for some formulas, the size of the truth table is exponentially larger than the size
of the formula. Consequently, this does not give a practical way to check satisfiability. Just
check how many rows that is for n = 1000, because it's common, for example, in computer
hardware verification applications to have more than 1000 variables.
Another way is to find an equivalent formula 0' in DNF. Now, the construction given
in the proof of Theorem 1 (Section 2.5.1) requires writing down the truth table for •, so
that method is too slow. Maybe, however, there is a faster way to find such a formula •' in
DNF. If so, that may provide a way to check satisfiability. Unfortunately, this approach also
is not, in general, practical: The shortest such formula 0' may itself be far longer than 0.
It turns out that there is a reasonably fast algorithm for checking satisfiability for CNF
formulas
0 = ()X0 V XI) A (P 2 V ;- 3 ) A ... A (X2n V X2n+l)where each clause contains at most two literals-formulas in what is called 2-CNE
However, if the clauses are allowed to contain even three literals (3-CNF), then the an-
swer is unknown. This problem is called the 3-satisfiability problem.
The 3-satisfiability problem is one of a large group of problems called H/P-complete
problems, which will be discussed further in Section 5.3.5. Another famous AHP-complete
problem is a form of the traveling salesperson problem, which will be discussed in Chapter
7. The commonly believed conjecture, called the P A HP conjecture, is that no HVP-
complete problems can be solved, in general, by algorithms that are even remotely prac-
tical. However, the conjecture is neither proved nor disproved (at least as of the time this
book was written), and it appears to be a very hard mathematical problem. It is considered
by many to be the most important unsolved problem in theoretical computer science-and
one of the most important unsolved problems in all of mathematics.
2.5.7 Resolution Proofs: Automating Logic
The ancient dream of automating reasoning will require a computer program to be able to
arrive at conclusions using rules of inference such as those shown in Table 2.6. One attempt
to automate reasoning in a special context was made by John R. Robinson, who used a
single inference rule called resolution. This inference rule deals exclusively with formulas
in CNF (clauses). As a simple example of this inference rule, called the resolution rule,
suppose the two clauses