Overview Of Direct Dnf To Cnf Conversion

variable names to their integer values in algen. These are respectively 0 and [] for the case of Tt. Formula Ff is handled similarly. A propositional variable is converted by the code under Pv(s). We look up s in the association list var_al, and if found, generate its CNF with respect to the looked-up result. Else, we generate a CNF clause containing next_var_int, the next variable to be allocated, and also return nvgen=1 and algen suitably records the association between s and next_var_int.
The remaining cases with propositional connectives are handled as shown: for And, we recursively convert its arguments, and call doAnd (Figure 18.3). The first four cases of doAnd deal with one of the arguments being false or true. The last case simply appends cnf1 and cnf2, as they are already in CNF form. In case of doOr, we perform a more elaborate case analysis. The case
| ([cl1],[cl2]) -> [List.append(cl1)(cl2)]
corresponds to two CNF clauses; here, we simply append the list of disjuncts to form a longer list of disjuncts. Given the case
| (cnf1’,[cl2]) -> doOr([cl2])(cnf1’)
This helps bring the first argument towards a single clause, at which time we can apply the append rule described earlier. Let us discuss the last case:
| (cnf1’, (cl2::cls)) ->
let door1 = doOr(cnf1’)([cl2]) in
let door2 = doOr(cnf1’)(cls) in
doAnd(door1)(door2) )
We recursively OR cnf1’ with the head of the second list, namely cl2, and the tail of the list, namely cls, and call doAnd on the result.