World's most popular travel blog for travel bloggers.

[Solved]: What is the state of the art in efficient boolean function operations?

, ,
Problem Detail:

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?

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).