SKEDSOFT
- Consider Figure 18.3 in which some terms representing DNF formulas are given. In particular, note that formula f5 is a 4-DNF formula with eight product terms. The expression List.length ( gencnf( f5 ) 1 [] ).cnf converts this formula to CNF, and measures its length, which is found to be 65536, showing the exponential growth in length. Here is a brief explanation of this code.
- In Figure 18.2, the types for literals, clauses, and CNF formulas are given. The Ocaml List of lists [[1; 3; -2]; [1; -1]] stands for the CNF formula (x1 ∨ x3 ∨ ¬x2) ∧ (x1 ∨ ¬x1). The syntax of formulas, fmla, declares what formula terms are permissible. According to these conventions, true is represented by [], i.e., an empty list of clauses, while false is represented by [[]], i.e., one empty clause.
- The program proceeds driven by pattern matching. Suppose fmla matches true (Tt); this results in an Ocaml record structure as shown in the following line: Tt -> {cnf=[ ]; nvgen=0; algen=[]}
- Note that [] is how true is represented. This is a list of lists with the outer list empty. Since the outer list is a list of conjunctions, an empty outer list corresponds to the basis case of a list of conjunctions, namely true. Likewise, [[]] represents false because the inner list is empty, and its basis case (for a list of disjunctions) is false (Ff). We also record the number of new variables generated in nvgen, and an association list of
