Pairwise (partial) equivalence of boolean functions

Question

I have a bunch of boolean functions, say $b_1,b_2,\dots,b_k \colon \{0,1\}^m \to \{0,1\}^n$, all given in terms of circuits.

I want to determine for which inputs they pairwise agree, that is, I want to compute, for all $b_i, b_j$ with $i \neq j$ the set $X_{i,j} \subseteq \{0,1\}^m$ of inputs such that $b_i(x) = b_j(x)$ for all $x \in X_{i,j}$ and $b_i(x) \neq b_j(x)$ for all $x \not\in X_{i,j}$. The question now is what is the most efficient way to do this in practice.

At the moment, my (naive) approach is to compute, for each pair $(i,j)$, the CNF-formula for $b_i \wedge b_j$ and then use a SAT solver to enumerate all models of this formula. This works but requires (at least) quadratically many SAT calls (at least one call for each pair $(i,j)$).

Now I am wondering if there is a better approach by transforming the $b_i$ first into some normal form, so that I can then compare these normal forms cheaply. One possibility would be to compute the full truth table for all $b_i$ (saved as a bitvector, for example). Then the comparison of $b_i$ and $b_j$ would boil down to simply AND-ing their bitvector representations (which is essentially for free). But the problem with this approach is that computing the full truth tables might be too expensive (when $m$ gets larger).

These two approach are somewhat orthogonal: The SAT approach requires little to no preprocessing but a lot of work for the comparisons. The truth table approach requires a lot of work for the preprocessing (= computing the truth tables), but the comparisons are then essentially for free.

Ideally, I am looking for some intermediate approach, where I put in some work in the beginning (computing some normal forms of the $b_i$) and then put in some work for the comparisons.

Anybody aware of any good approaches for my problem?

Answer 1

The approach you hint in the end is actually one focus of a field known as knowledge compilation. Here, the goal is to transform a "bad" (in the sense, hard to do anything with it) representation of a Boolean function into a "good" one (in the sense, it enjoys good properties).

One noticeable data structure to represent Boolean function is OBDD. If all your functions are encoded as OBDDs using the same underlying variable order, then you can compute what you need efficiently. Indeed, if $F$ and $G$ are two OBDDs of size $N_F$, $N_G$ and sharing the same variables order, you can compute an OBDD for $F \wedge G$ of size at most $N_FN_G$. This OBDD represents all assignments you are interested in and can now be used to enumerate them, or count them etc.

Many generalizations of OBDD have been studied in knowledge compilation [5]. The jargon may be a bit offsetting at first but what you will be interested in is to transform your boolean functions into data structures efficiently supporting the operation "APPLY" which roughly boils down to combine two data structures for $f$ and $g$ respectively into one computing $f \wedge g$.

This includes :

• OBDD [1,2]
• structured d-DNNF [3]
• SDD [4]

Tools for these languages exist, see for example CuDD (https://github.com/ivmai/cudd) or SDD (http://reasoning.cs.ucla.edu/sdd/).

That should be faster than generating the whole truth table (you can see these data structures as some kind of "factorized" version of the truth table) and will give you a representation of the intersection that is more compact than the full list of assignments without compromising tractability of many tasks. That said, depending on what your instances look like, the SAT solver approach you mention may sometimes be better, though listing every assignment of $b_i \wedge b_j$ may still be more efficiently done using a knowledge compiler which can then be used to output every model. In this case, you do not need to have the APPLY procedure and can use more general data structure (e.g, decDNNF or d-DNNF, check tool d4 for instance https://github.com/crillab/d4v2).

References

[1] Bryant, R. E. (1992). Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys (CSUR), 24(3), 293-318. BRYANT, Randal E. Symbolic boolean manipulation with ordered binary-decision diagrams.

[2] Wegener, I. (2000). Branching programs and binary decision diagrams: theory and applications. Society for Industrial and Applied Mathematics.

[3] Pipatsrisawat, K., & Darwiche, A. (2010). Top-down algorithms for constructing structured DNNF: Theoretical and practical implications. In ECAI 2010 (pp. 3-8). IOS Press.

[4] Darwiche, A. (2011, June). SDD: A new canonical representation of propositional knowledge bases. In Twenty-Second International Joint Conference on Artificial Intelligence.

[5] Darwiche, A., & Marquis, P. (2002). A knowledge compilation map. Journal of Artificial Intelligence Research, 17, 229-264.

Answer 2

I suggest you try binary decision diagrams. A BDD is a representation of a boolean function.

Given BDDs for $f,g$, you can compute a BDD for $f = g$ (i.e., for $f \oplus g \oplus 1$, where $\oplus$ represents XOR) efficiently (in at most quadratic time). Also, given a BDD for a binary function $f$, you can fairly efficiently enumerate the set $\{x \mid f(x)=1\}$ of inputs that cause the circuit to output 1.

So, the preprocessing work will be to convert each $b_i$ to a BDD. This should make it more efficient to compute $X_{i,j}$ (as the set of inputs that cause $b_i \oplus b_j \oplus 1$ to output 1). There are existing software libraries for working with BDDs.