ABSTRACT
In this chapter we look at the effects of changing representations of clauses and of sets of clauses. We will explore (but this is, literally, “the tip of the iceberg”) the results of representing clauses and sets of clauses in two formalisms: linear programming (but really in integer programming) and matrix algebra. In the first of these areas, we represent each clause as an inequality. As the result, the sets of clauses are represented by systems of inequalities. The basic idea here is to identify Boolean values 0 and 1 with integers 0 and 1 (nothing strange in itself; something similar happens in some programming languages). This representation is faithful in the following sense: the solutions to the resulting sets of inequalities, as long as they are in the desired form, taking only values 0 and 1, can be “pulled back,” resulting in satisfying valuations for the original CNF. In fact, we will see that there is more than one representation of clausal logic in the integer programming. The second representation, closer in spirit to Kleene three-valued logic, requires solutions taking only values −1 and 1. The simple act of conversion brings, however, advantages: techniques applicable in integer programming can be used to locate satisfying valuations.
