|
|
PROG
| The following program generates all truth tables of k-CNF expressions of n variables:
start with the truth table (2^2^n) - 1 //e.g., 0xFFFF for n=4
for each new truth table //e.g., 0xFFFF
for each (n choose k) variables //e.g., a, c, d
for each (2^k) clause of these variables //e.g., (a or not c or not d)
generate a truth table from the clause and previous truth table //e.g., NewTT = PrevTT and (...)
Bit operations allow an efficient implementation of the last step. If you represent each variable by its truth table, A, B, ..., in 1-CNF, then the last step is 'NewTT = PrevTT and (A or B or C ...)'. For example, with four variables a, b, c and d, the 1-CNF truth table for 'a' is 0xFF00, 'not c' is 0x3333 and 'not d' is 0x5555. The corresponding step is 'NewTT = PrevTT and 0xFFBB'.
|
