ABSTRACT
In this chapter we will discuss the issues associated with the use of SAT (i.e., satisfiability) for actual computation. The idea is to use the propositional logic (and its close relative, predicate logic) as knowledge representation language. We will assume that we have a piece of software, called solver, which does the following: it accepts CNFs (say, F ) and returns a string ‘Input theory unsatisfiable’ or a satisfying valuation for F . We will assume that solver is correct and complete. That is, if there is a satisfying valuation v for F , it returns one. If there is none, it returns the string ‘Input theory unsatisfiable.’ This is an idealized situation for a variety of reasons. First, F itself may be too big to be handled by the program solver. Second, since our resources are finite, it may be that the program solver will need more time for processing F than we have (after all, we all sooner or later expire, and DPLL searches the entire tree of partial valuations of Var which is exponential in the size of Var ). Third, solver, and this is a minor, but very real, issue, like every humanly written program, may have bugs. But we will assume that we live in an ideal world. Arbitrary large finite CNFs are accepted, the solver returns the solution (if one exists) immediately, and solver is a correct implementation of DPLL or any other complete algorithm for SAT.
