URL: http://www.qhull.org/ttncf
Ttcnf computes all truth tables of CNF boolean expressions with one to five variables. It counts these truth tables in a number of ways. These results may be useful in understanding CNF expressions.
The following sections define the ttcnf program and summarize the results for 1-CNF, 2-CNF, 3-CNF, 4-CNF, (n-1)-CNF, n-CNF, and CNF.
The ttcnf program is a C/assembler program compiled for Windows. For a list of options, run 'ttcnf'. For five variables, it needs a gigabyte of data. It runs well on a two gigabyte computer. The output of ttcnf is comma-delineated text. View the output with Excel using Window>FreezePanes to keep the header visible.
A truth table is a enumeration of n boolean variables and the result of executing a boolean function of these variables. For example, the truth table for x and y is:
x y x and y 0 0 0 0 1 0 1 0 0 1 1 1
Since the input enumeration is mechanical, the result column defines the truth table and the corresponding boolean function. In the previous truth table, the result column is the number 0x8 in hexadecimal or 0b1000 in binary.
Conjunctive normal form (CNF) is a canonical representation of boolean functions. CNF is the conjunction of disjunctive clauses. Disjunctive clauses use the not and or operators, while conjunction is the and operator. A CNF expression is k-CNF if each clause contains k variables. An example of 2-CNF is (a or b) and (not c or d).
A CNF expression is satisfiable if there exists an assignment of variables for which the expression is true. For example, (a or b) and (not c or d) is true if a and d are true.
k-SAT is the problem of testing satisfiability for k-CNF expressions. Clearly k-SAT can be solved by testing each possible assignment of the variables. Is there a faster way? There is a faster way if k<3, but it appears to be false for other k.
Ttcnf explored the possibility that 3-CNF produced so many truth tables that it had to include random truth tables. If so, the mapping from 3-CNF to truth table would have to be random, requiring exhaustive testing of the inputs. This does not appear to be the case.
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 0xFF77'.
If the last step takes unit time, the space and time complexity is O(2^2^n) and O(2^2^n * (n choose k) * 2^k) respectively, For 3-CNF truth tables of n variables, the space and time complexity is
n Space Time 3 2^8 2^11 4 2^16 2^21 5 2^32 2^38 6 2^64 2^71
Knuth counted the truth tables for 3-CNF in six variables by converting the problem to a system of constraints solved as a BDD (binary decision diagram).
For 1-CNF, two clauses always produces a contradiction and hence a non-satisfiable expression (e.g., a and not a).
The first column is the number of unique truth tables generated by 1-CNF expressions. The second column is the total number of truth tables (i.e., 2^2^n). The first column of the second table is the maximum number of clauses in a 1-CNF expression that generates a unique truth table. The second column is the minimum number of clauses in a non-satisfiable 1-CNF expression. The last column is the number of clauses that generates at least half of the unique truth tables.
n 1-CNF truth tables All truth tables 1 2 2 2 10 16 3 28 256 4 82 65,536 5 244 4,294,967.296
n 1-CNF clauses clauses to
first non-SATclauses to half of
the truth tables2 2 2 1 3 3 2 2 4 4 2 3 5 5 2 3
n 2-CNF truth tables All truth tables 2 16 16 3 166 256 4 4,170 65,536 5 224,716 4,294,967.296
n 2-CNF clauses clauses to
first non-SATclauses to half of
the truth tables2 4 4 2 3 5 4 3 4 6 4 4 5 10 4 5
n 3-CNF truth tables All truth tables 3 256 256 4 43,146 65,536 5 120,510,132 4,294,967.296
n 3-CNF clauses clauses to
first non-SATclauses to half of
the truth tables3 8 8 4 4 8 8 5 5 12 8 7
n 4-CNF truth tables All truth tables 4 65,536 65,536 5 2,805,252,934 4,294,967.296
n 4-CNF clauses clauses to
first non-SATclauses to half of
the truth tables4 16 16 8 5 16 16 9
In (n-1)-CNF, each clause has n-1 variables.
n (n-1)-CNF truth tables All truth tables 2 10 16 3 166 256 4 43,146 65,536 5 2,805,252,934 4,294,967.296
n (n-1)-CNF clauses clauses to
first non-SATclauses to half of
the truth tables2 2 2 1 3 4 4 3 4 8 8 5 5 16 16 9
In n-CNF, each clause has n variables. An n-CNF expression is a simple transformation of a truth table. Each distinct clause of an n-CNF expression corresponds to a 0-bit of the truth table. For example, bit 1 of the truth table for four variables is zero if and only if the n-CNF expression includes the clause 'a or b or c or not d'. Since a satisfiable expression contains at least one 1-bit in its truth table, n-CNF is satisfiable if and only if it is not 2^n distinct clauses.
As expected for n-CNF, ttcnf generates every truth table in 2^n clauses. The last clause generates truth table 0x0.
n n-CNF truth tables All truth tables 1 2 2 2 16 16 3 256 256 4 65,536 65,536 5 4,294,967.296 4,294,967.296
n n-CNF clauses clauses to
first non-SATclauses to half of
the truth tables2 4 4 2 3 8 8 4 4 16 16 8 5 32 32 16
n CNF truth tables All truth tables 1 2 2 2 16 16 3 256 256 4 65,536 65,536 5 4,294,967.296 4,294,967.296
n CNF clauses clauses to
first non-SATclauses to half of
the truth tables2 2 2 1 3 4 2 2 4 8 2 4 5 16 2 7
To test mixed 3-CNF and 2-CNF expressions, the 'keep' option for ttcnf can generate all 2-CNF expressions followed by one or more 3-CNF clauses. Pre-loading the truth tables with 2-CNF allows 3-CNF to converge slightly faster. Instead of generating all truth tables from 0xFFFFFF..., it has many starting points, one for each 2-CNF truth table.
For four and five variables, the 2-CNF clauses do not make a big difference. The same number of 3-CNF clauses are required to generate all of the truth tables. To generate half of the truth tables, two fewer clauses are required for four variables and one fewer clause for five variables.
Allowing any mix of 3-CNF and 2-CNF clauses behaves like 3-CNF alone (options 'kcnf 0x0305' and 'kcnf 0x0306' for n=4 and n=5 respectively). For five variables, it requires one fewer clause to generate half of the truth tables.
The number of new truth tables fits a Gaussian distribution. For 3-CNF, GraphPad computed the fit with an R^2 of 0.999 (see the previous links). The Gaussian distribution is visibly apparent, e.g. for 3-CNF of four variables:
num. clauses new truth tables 0 1 1 32 2 472 3 3392 4 11204 5 15184 6 9568 7 2928 8 365 9 0
The ttcnf program has several bucketing options for counting truth tables. For example, 'nibble 3' divides the truth tables into 16 buckets by the nibble starting at bit 3. None of these options were helpful. The most interesting was 'lownibble'.
Consider a nibble of the bit string representing a truth table. For example, for 4 variables, a,b,c,d, consider nibble 'F' of 0x000F (the truth table for 'not a and not b').
With (n-1)-CNF the first n-2 variables can isolate a nibble, allowing the remaining variable to set the nibble to 0x3, 0x5, 0xa, 0xc. With two such clauses, the nibble may be set to 0x0, 0x1, 0x2, 0x4, and 0x8. With no clause, the nibble may be left at 0xf. Call these nibbles, the low nibbles (0x0,0x1,0x2,0x3,0x4,0x5,0x8,0xa,0xc,0xf). So, (n-1)-CNF can create any truth table composed of the low nibbles (e.g., 0x3cf2).
The option 'lownibble' shows the effect of low nibbles on truth tables. If a truth table contains a high nibble, it is assigned to the highest bucket, otherwise it is assigned to bucket i if it contains i non-zero low nibbles. For example, the truth table 0x3c02 is assigned to bucket 3.
For (n-1)-CNF there are 2^(n-2) nibbles with each nibble having one of ten values. So the number of low nibble truth tables is 10^(2^(n-2)). For four variables, low nibbles accounts for 23% of the (n-1)-CNF truth tables (10,000 out of 43,146). For five variables, low nibbles accounts for 3.6% of the truth tables (100,000,000 out of 2,805,252,934). It appears that low nibbles are decreasingly important as the number of variables increases. For (n-2)-CNF, the same construction applies to bytes instead of nibbles. While low-bytes can be identified, they only account for about 100,000 truth tables when n=5.
Boolean expressions are equivalent under negation and permutation. This leads to regularities in the number of truth tables in a bucket. For example, if buckets are defined by the middle byte (0x000ff000), the same number of truth tables occurs for multiple buckets. For example, buckets (0b01100110 and 0b10011001) both have 161794 truth tables.
Number of truth tables for 256 buckets 0x000ff000
First bucket 0s n tables total description 01101001 4 2 53881 107762 complement with four 0s 11111111 0 1 126280 126280 all 1 01100110 4 2 161794 323588 complement with four 0s 01110111 2 4 134392 537568 reverse + rotate one 01101111 2 4 148192 592768 symmetric with two 0s, >>2 01111110 2 4 148615 594460 symmetric with two 0s 01101011 3 8 89017 712136 8-fold with three 0s 01111011 2 8 108256 866048 8-fold with two 0s 01111111 1 8 132742 1061936 8 rotations 00110011 4 4 288061 1152244 complement with four 0s, 0011 and 0101 01100111 3 8 153925 1231400 8 rotations 00000110 6 4 466569 1866276 0000 plus 0110 and 1001 00010110 5 8 242848 1942784 8-fold with reversals 00001111 4 2 1007948 2015896 complements of 0000 00111111 2 8 257240 2057920 1111 plus 00..11 and 11..00 00010111 4 8 265629 2125032 8-fold with four 0s 00011001 5 8 272026 2176208 8-fold with five 0s 00010001 6 4 601045 2404180 rotations of 10001000 00111100 4 4 679114 2716456 complements with four 0s 00110111 3 16 189837 3037392 16-fold with three 0s 00011110 4 8 390002 3120016 complement with four 0s 00110110 4 16 200563 3209008 16-fold with four 0s 00011111 4 8 445133 3561064 1111 plus rotations of 1000 00110101 4 8 445259 3562072 complement with four 0s 00111101 3 16 271888 4350208 16-fold with three 0s 00011000 6 4 1110913 4443652 counter rotation of 0001 and 1000 00000000 8 1 5243626 5243626 all 0 00000111 5 8 672063 5376504 0000 plus rotations of 0111 00011011 4 16 348070 5569120 16-fold with four 0s 00010010 6 8 840481 6723848 counter rotations of 0001 and 0010 00010011 5 16 500821 8013136 16-fold with five 0s 00000011 6 8 1434074 11472592 0000 plus 1100 and 0101 with complements 00011010 5 16 819809 13116944 16-fold with five 0s 00000001 7 8 1887501 15100008 rotations of 00000001 total 120510132
If you select the truth tables in one of the groups, and bucket on a different byte, a similar pattern occurs.
Number of truth tables for 256 buckets (0x000000ff) for truth tables with 348070 truth tables in bucket 0x000ff000 (00011011)
First bucket 0s n tables total description 01101001 4 2 0 0 complement with four 0s 01101011 3 8 0 0 8-fold with three 0s 01101111 2 4 2304 9216 symmetric with two 0s, >>2 01111011 2 8 1370 10960 8-fold with two 0s 01111110 2 4 3656 14624 symmetric with two 0s 11111111 0 1 15232 15232 all 1 00010110 5 8 4000 32000 8-fold with reversals 00011110 4 8 4812 38496 complement with four 0s 01100110 4 2 20856 41712 complement with four 0s 01111111 1 8 6494 51952 8 rotations 00111100 4 4 13436 53744 complements with four 0s 01100111 3 8 8166 65328 8 rotations 01110111 2 4 17152 68608 reverse + rotate one 00001111 4 2 35104 70208 complements of 0000 00011000 6 4 21492 85968 counter rotation of 0001 and 1000 00110110 4 16 5790 92640 16-fold with four 0s 00010111 4 8 12058 96464 8-fold with four 0s 00011111 3 8 12142 97136 1111 plus rotations of 1000 00111101 3 16 6418 102688 16-fold with three 0s 00111111 2 8 13224 105792 1111 plus 00..11 and 11..00 00110101 4 8 13712 109696 complement with four 0s 00011001 5 8 19808 158464 8-fold with five 0s 00000110 6 4 39816 159264 0000 plus 0110 and 1001 00110011 4 4 43276 173104 complement with four 0s, 0011 and 0101 00000000 8 1 175632 175632 all 0 00110111 3 16 14089 225424 16-fold with three 0s 00011010 5 16 14959 239344 16-fold with five 0s 00010010 6 8 31618 252944 counter rotations of 0001 and 0010 00011011 4 16 16238 259808 16-fold with four 0s 00000111 5 8 38010 304080 0000 plus rotations of 0111 00010001 6 4 80192 320768 rotations of 10001000 00010011 5 16 37738 603808 16-fold with five 0s 00000011 6 8 78022 624176 0000 plus 1100 and 0101 with complements 00000001 7 8 113730 909840 rotations of 00000001 total 5569120
[Jan 2014] ttcnf-2014.1.zip -- Minor improvements.
[Dec 2012] D. Knuth extended sequence A112535 to six variables by solving a system of constraints as a BDD.
[Nov 2009] W. Chen corrected the NewTT example in "The ttcnf program" and the clauses column of "Curve fit".
[Dec 2005] A112535 -- Sequence for number of truth tables in 3-CNF
[Apr 2005] ttcnf-2005.1.zip -- Original release