URL: http://www.qhull.org/ttncf


[ttcnf-3-new] ttcnf - Truth Table CNF

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.

Truth tables, CNF expressions, and satisfiability

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 ttcnf program

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
32^82^11
42^162^21
52^322^38
62^642^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).

Results for 1-CNF

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
122
21016
328256
48265,536
52444,294,967.296
n    1-CNF clausesclauses to
    first non-SAT
    clauses to half of
the truth tables
2221
3322
4423
5523

Results for 2-CNF

For 2-CNF, four clauses generates a contradiction (e.g., (a or b) and (not a or b) and (a or not b) and (not a or not b)).
n    2-CNF truth tables    All truth tables
21616
3166256
44,17065,536
5224,7164,294,967.296
n    2-CNF clausesclauses to
    first non-SAT
    clauses to half of
the truth tables
2442
3543
4644
51045

Results for 3-CNF

n    3-CNF truth tables    All truth tables
3256256
443,14665,536
5120,510,1324,294,967.296
n    3-CNF clausesclauses to
    first non-SAT
    clauses to half of
the truth tables
3884
4885
51287

Results for 4-CNF

n    4-CNF truth tables    All truth tables
465,53665,536
52,805,252,9344,294,967.296
n    4-CNF clausesclauses to
    first non-SAT
    clauses to half of
the truth tables
416168
516169

Results for (n-1)-CNF

In (n-1)-CNF, each clause has n-1 variables.

n    (n-1)-CNF truth tables    All truth tables
21016
3166256
443,14665,536
52,805,252,9344,294,967.296
n    (n-1)-CNF clausesclauses to
    first non-SAT
    clauses to half of
the truth tables
2221
3443
4885
516169

Results for n-CNF

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
122
21616
3256256
465,53665,536
54,294,967.2964,294,967.296
n    n-CNF clausesclauses to
    first non-SAT
    clauses to half of
the truth tables
2442
3884
416168
5323216

Results for CNF

A CNF expression has multiple lengths of clauses (e.g, 1-CNF, 2-CNF, ..., 5-CNF). This shortens the number of clauses, but does not change the generated truth tables. Compared to n-CNF, it cuts the number of clauses by half.
n    CNF truth tables    All truth tables
122
21616
3256256
465,53665,536
54,294,967.2964,294,967.296
n    CNF clausesclauses to
    first non-SAT
    clauses to half of
the truth tables
2221
3422
4824
51627

Results for 3-CNF with 2-CNF

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.

Curve fit for new 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
01
132
2472
33392
411204
515184
69568
72928
8365
90

Results for bucketing

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.

Results for bucketing for truth tables of 3-CNF in five variables

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 0sntablestotaldescription
0110100142 53881 107762complement with four 0s
1111111101 126280126280all 1
0110011042 161794323588complement with four 0s
0111011124 134392537568reverse + rotate one
0110111124 148192592768symmetric with two 0s, >>2
0111111024 148615594460symmetric with two 0s
0110101138 89017 7121368-fold with three 0s
0111101128 1082568660488-fold with two 0s
0111111118 13274210619368 rotations
0011001144 2880611152244complement with four 0s, 0011 and 0101
0110011138 15392512314008 rotations
0000011064 46656918662760000 plus 0110 and 1001
0001011058 24284819427848-fold with reversals
000011114210079482015896complements of 0000
0011111128 25724020579201111 plus 00..11 and 11..00
0001011148 26562921250328-fold with four 0s
0001100158 27202621762088-fold with five 0s
0001000164 6010452404180rotations of 10001000
0011110044 6791142716456complements with four 0s
00110111316189837303739216-fold with three 0s
0001111048 3900023120016complement with four 0s
00110110416200563320900816-fold with four 0s
0001111148 44513335610641111 plus rotations of 1000
0011010148 4452593562072complement with four 0s
00111101316271888435020816-fold with three 0s
0001100064 11109134443652counter rotation of 0001 and 1000
0000000081 52436265243626all 0
0000011158 67206353765040000 plus rotations of 0111
00011011416348070556912016-fold with four 0s
0001001068 8404816723848counter rotations of 0001 and 0010
00010011516500821801313616-fold with five 0s
0000001168 1434074 114725920000 plus 1100 and 0101 with complements
000110105168198091311694416-fold with five 0s
0000000178 188750115100008rotations 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 0sntablestotaldescription
011010014 2 0 0complement with four 0s
011010113 8 0 08-fold with three 0s
011011112 4 2304 9216symmetric with two 0s, >>2
011110112 8 1370 109608-fold with two 0s
011111102 4 3656 14624symmetric with two 0s
111111110 1 15232 15232all 1
000101105 8 4000 320008-fold with reversals
000111104 8 4812 38496complement with four 0s
011001104 2 20856 41712complement with four 0s
011111111 8 6494 519528 rotations
001111004 4 13436 53744complements with four 0s
011001113 8 8166 653288 rotations
011101112 4 17152 68608reverse + rotate one
000011114 2 35104 70208complements of 0000
000110006 4 21492 85968counter rotation of 0001 and 1000
00110110416 5790 9264016-fold with four 0s
000101114 8 12058 964648-fold with four 0s
000111113 8 12142 971361111 plus rotations of 1000
00111101316 641810268816-fold with three 0s
001111112 8 132241057921111 plus 00..11 and 11..00
001101014 8 13712109696complement with four 0s
000110015 8 198081584648-fold with five 0s
000001106 4 398161592640000 plus 0110 and 1001
001100114 4 43276173104complement with four 0s, 0011 and 0101
000000008 1 175632175632all 0
00110111316 1408922542416-fold with three 0s
00011010516 1495923934416-fold with five 0s
000100106 8 31618252944counter rotations of 0001 and 0010
00011011416 1623825980816-fold with four 0s
000001115 8 380103040800000 plus rotations of 0111
000100016 4 80192320768rotations of 10001000
00010011516 3773860380816-fold with five 0s
000000116 8 780226241760000 plus 1100 and 0101 with complements
000000017 8 113730909840rotations of 00000001
total 5569120

History

[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