# What is the state of the art in efficient boolean function operations?

How do you most efficiently combine boolean functions with a large number of variables using AND, OR, and NOT? The most up-to-date work that I can find on this subject is about 20 years old (Efficient data structures for Boolean functions). Which search terms should I be using to explore this question?

Edit:

I am starting from about 200 simple boolean functions. These are combined with each other using AND, OR, NOT, and XOR to give other boolean functions, which are then also combined using AND, OR, NOT, and XOR. The process repeats about 3000 times, until a final combination gives me a single boolean expression. I'm interested in that final expression.

Representing the functions as DNF or CNF makes certain operations (NOT and XOR) slow. Representing the functions as ROBDDs is an option - are there any drawbacks here? I'm not sure whether SMT solvers are useful here, because I am interested in the final equation rather than whether the equation is satisfiable. What else should I be looking at?

• What do you mean by "efficiently combining"? Also, this seems quite broad. Community, your votes? – Raphael Jun 25 '14 at 13:04
• Is it possible that by "combine" you mean reduce, simplify, or the like? That is, are you trying to turn $f(a, b) = a + ab$ into $f(a, b) = a$? Or is what you're asking about efficiently evaluating expressions - i.e., determining the value of $a + ab$ is $T$ if $a$ is (without evaluating $ab$)? – Patrick87 Jun 25 '14 at 16:17
• Or maybe this? en.wikipedia.org/wiki/Binary_decision_diagram – Wandering Logic Jun 25 '14 at 18:03
• In particular the reference to Knuth vol 4, which should bring you up to the state of the art as of 5 or 10 years ago. – Wandering Logic Jun 25 '14 at 18:44
• This post needs to be edited to make question more clear and easier to understand. – Kaveh Aug 11 '14 at 16:51

The obvious method is to use BDDs.

Given a BDD for two boolean functions $f,g$, you can form a BDD for $f \land g$, $f \lor g$, $\neg f$, $f \implies g$, $f \oplus g$ (xor), and many other binary operations on them. Also, given BDDs for $f,g$, you can test whether $f$ and $g$ are the same boolean function.

The worst-case behavior is that their size might grow to be exponential in $n$, the number of boolean variables, but empirically, the size often remains manageable in many real-world applications, e.g., when there is suitable structure in the underlying boolean functions. In the model-checking world, designs with 50-200 boolean variables are routinely handled using BDDs.

It's also possible to manipulate boolean expressions in symbolic form, and then use SAT solvers or SMT solvers to test for equivalence. This is another plausible alternative.

My advice is: try BDDs first, then if they don't scale well enough for your needs, you can try SAT-based solutions. If that still doesn't work, come back to ask for more suggestions (providing more details about your specific setting and what you've tried).

try also ZDDs (Zero-suppressed Decision Diagrams) for "sparse" functions where most evaluations are zero and subject to more recent research. Knuth has researched/implemented them and regards them highly, and compressions can be dramatically better in some applications. see also Minato for a survey/ contrast with BDDs & a database application.