CNF by truth table

Question

I have a Boolean function over 10 variables, represented explicitly by a truth table. Only a small number of inputs evaluate to True, so most of the 2^10=1024 input combinations are False.

I'd like to convert this function to CNF (Conjunctive Normal Form) — not necessarily the smallest possible CNF, but one that is reasonably compact and efficient to use in downstream tools (e.g., SAT solvers).

What I’ve tried:

Blocking false assignments: A straightforward method is to write one clause for each input that results in False, but this becomes impractical when there are only a few True outputs.

From True models (DNF to CNF): I tried creating a DNF by taking each True assignment and forming a conjunction of its literals. Then, converting this DNF to CNF by generating clause products and pruning:

• Filter out contradictory clause products,
• Remove redundant supersets.

But even with pruning, the number of intermediate combinations can grow up to 10^t, where t is the number of True assignments — making this approach infeasible for larger t.

Is there any other approach that can be used to solve this problem?

Answer 1

The sympy package allows you to do this out-of-the box. (https://www.sympy.org/en/index.html)

Here's a simple example. Assuming you've three variables and the truth table encodes the following set:

  (x & y & !z) \/ (x & !y & z)

(i.e., only the rows corresponding to x=true, y=true, z=false and x=true, y=false, z=true are true, while all others are false). You can easily code this and convert to CNF as follows:

$ python3
Python 3.8.5 (default, Jul 21 2020, 10:48:26)
[Clang 11.0.3 (clang-1103.0.32.62)] on darwin
Type "help", "copyright", "credits" or "license" for more information.
>>> from sympy import *
>>> x, y, z = symbols('x y z')
>>> simplify_logic((x & y & ~z) | (x & ~y & z), form="cnf")
x & (y | z) & (~y | ~z)

simplify_logic can convert to CNF or DNF, based on the form argument. See here: https://github.com/sympy/sympy/blob/c3087c883be02ad228820ff714ad6eb9af1ad868/sympy/logic/boolalg.py#L2746-L2827

Note that CNF expansion can be costly in general, and Tseitin encoding is the preferred method to avoid this complexity (https://en.wikipedia.org/wiki/Tseytin_transformation). But it has the disadvantage of introducing new variables.