ABSTRACT
This chapter is the first of four that are devoted to issues in knowledge representation. While knowledge representation is an area with practical applications, in this chapter we start with a construction that is theoretical, but carries an important promise. Specifically, in this chapter we encode the problem of Turing machines reaching the final state as a satisfiability problem. To prove that SAT is NP-complete, we will reduce to SAT any language decided by a nondeterministic Turing machine in polynomial time. We need to be very careful so that the reader does not get the impression that SAT solves the halting problem. What we show is that if we set the bound on the length of the run of the machine then the problem of reaching the final state within such bound can be represented as a SAT problem. In fact, we will find a polynomial f(·) such that the size of the SAT problem solving this limited halting problem is bound by f(|M | + |I| + k), where |M | is the size of the machine, |I| is the size of the input, and k is the bound on the number of steps allowed until we reach the final state. One consequence of this coding (and proof of correctness of coding) is that every problem in the class NP polynomially reduces to SAT. Thus the message of this chapter is that, at least in principle, SAT can serve as a universal tool for encoding search problems in the class NP. Next, we also show that we can polynomially reduce satisfiability to satisfiability of sets of 3-clauses. We then show how circuits (and hence arbitrary formulas) can be coded into sets of clauses. We also show that the existence problem for autarkies is NP-complete. Finally, we show that “mix-and-match” of (most of) polynomial cases (studied in
of 21 cases (we refer to Chapter 9 for the definition of 7 “easy” cases) of pairs of “easy” theories, 19 cases lead to classes of CNFs for which the satisfiability problem is NP-complete, whereas two have polynomial complexity. We refer the reader to the book by M. Sipser [Sip06], Chapter 7, especially Section 7.3, for relevant definitions.
