<p>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 &quot;bad&quot; (in the sense, hard to do anything with it) representation of a Boolean function into a &quot;good&quot; one (in the sense, it enjoys good properties).</p>
<p>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 <span class="math-container">$F$</span> and <span class="math-container">$G$</span> are two OBDDs of size <span class="math-container">$N_F$</span>, <span class="math-container">$N_G$</span> and sharing the same variables order, you can compute an OBDD for <span class="math-container">$F \wedge G$</span> of size at most <span class="math-container">$N_FN_G$</span>. This OBDD represents all assignments you are interested in and can now be used to enumerate them, or count them etc.</p>
<p>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 &quot;APPLY&quot; which roughly boils down to combine two data structures for <span class="math-container">$f$</span> and <span class="math-container">$g$</span> respectively into one computing <span class="math-container">$f \wedge g$</span>.</p>
<p>This includes :</p>
<ul>
<li>OBDD [1,2]</li>
<li>structured d-DNNF [3]</li>
<li>SDD [4]</li>
</ul>
<p>Tools for these languages exist, see for example CuDD (<a href="https://github.com/ivmai/cudd" rel="noreferrer">https://github.com/ivmai/cudd</a>) or SDD (<a href="http://reasoning.cs.ucla.edu/sdd/" rel="noreferrer">http://reasoning.cs.ucla.edu/sdd/</a>).</p>
<p>That should be faster than generating the whole truth table (you can see these data structures as some kind of &quot;factorized&quot; 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 <span class="math-container">$b_i \wedge b_j$</span> 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 <a href="https://github.com/crillab/d4v2" rel="noreferrer">https://github.com/crillab/d4v2</a>).</p>
<h1>References</h1>
<p>[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.</p>
<p>[2] Wegener, I. (2000). Branching programs and binary decision diagrams: theory and applications. Society for Industrial and Applied Mathematics.</p>
<p>[3] Pipatsrisawat, K., &amp; Darwiche, A. (2010). Top-down algorithms for constructing structured DNNF: Theoretical and practical implications. In ECAI 2010 (pp. 3-8). IOS Press.</p>
<p>[4] Darwiche, A. (2011, June). SDD: A new canonical representation of propositional knowledge bases. In Twenty-Second International Joint Conference on Artificial Intelligence.</p>
<p>[5] Darwiche, A., &amp; Marquis, P. (2002). A knowledge compilation map. Journal of Artificial Intelligence Research, 17, 229-264.</p>

CC BY-SA 4.0
2024-11-22T21:28:15.727Z
2024-11-22T21:28:15.727Z
holf
<p>I suggest you try <a href="https://en.wikipedia.org/wiki/Binary_decision_diagram" rel="noreferrer">binary decision diagrams</a>.  A BDD is a representation of a boolean function.</p>
<p>Given BDDs for <span class="math-container">$f,g$</span>, you can compute a BDD for <span class="math-container">$f = g$</span> (i.e., for <span class="math-container">$f \oplus g \oplus 1$</span>, where <span class="math-container">$\oplus$</span> represents XOR) efficiently (in at most quadratic time).  Also, given a BDD for a binary function <span class="math-container">$f$</span>, you can fairly efficiently enumerate the set <span class="math-container">$\{x \mid f(x)=1\}$</span> of inputs that cause the circuit to output 1.</p>
<p>So, the preprocessing work will be to convert each <span class="math-container">$b_i$</span> to a BDD.  This should make it more efficient to compute <span class="math-container">$X_{i,j}$</span> (as the set of inputs that cause <span class="math-container">$b_i \oplus b_j \oplus 1$</span> to output 1).  There are existing software libraries for working with BDDs.</p>

CC BY-SA 4.0
2024-11-24T09:56:38.497Z
While in the same spirit, this answer is actually better than mine since it addresses the OP problem of finding assignments where $b_i=b_j$ while mine is about finding assignments where both are true (I focused on the solution proposed by the OP and not on the core problem). So XORing the data structure is what you need, not the conjunction of course.
holf
CC BY-SA 4.0
2024-11-24T06:04:55.347Z
2024-11-24T06:04:55.347Z
D.W.
<p>I have a bunch of boolean functions, say <span class="math-container">$b_1,b_2,\dots,b_k \colon \{0,1\}^m \to \{0,1\}^n$</span>, all given in terms of circuits.</p>
<p>I want to determine for which inputs they pairwise agree, that is, I want to compute, for all <span class="math-container">$b_i, b_j$</span> with <span class="math-container">$i \neq j$</span> the set <span class="math-container">$X_{i,j} \subseteq \{0,1\}^m$</span> of inputs such that <span class="math-container">$b_i(x) = b_j(x)$</span> for all <span class="math-container">$x \in X_{i,j}$</span> and <span class="math-container">$b_i(x) \neq b_j(x)$</span> for all <span class="math-container">$x \not\in X_{i,j}$</span>. The question now is what is the most efficient way to do this in practice.</p>
<p>At the moment, my (naive) approach is to compute, for each pair <span class="math-container">$(i,j)$</span>, the CNF-formula for <span class="math-container">$b_i \wedge b_j$</span> 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 <span class="math-container">$(i,j)$</span>).</p>
<p>Now I am wondering if there is a better approach by transforming the <span class="math-container">$b_i$</span> 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 <span class="math-container">$b_i$</span> (saved as a bitvector, for example). Then the comparison of <span class="math-container">$b_i$</span> and <span class="math-container">$b_j$</span> 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 <span class="math-container">$m$</span> gets larger).</p>
<p>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.</p>
<p>Ideally, I am looking for some intermediate approach, where I put in some work in the beginning (computing some normal forms of the <span class="math-container">$b_i$</span>) and then put in some work for the comparisons.</p>
<p>Anybody aware of any good approaches for my problem?</p>

CC BY-SA 4.0
2024-11-22T21:42:46.717Z
Simultaneously cross-posted at https://cs.stackexchange.com/questions/170457/pairwise-partial-equivalence-of-boolean-functions .
Emil Jeřábek
<boolean-functions><boolean-formulas><equivalence>
Pairwise (partial) equivalence of boolean functions
Mens
# Pairwise (partial) equivalence of boolean functions

(Asked by: username_0 on 2024-11-22)

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?

**Tags:** boolean-functions, boolean-formulas, equivalence
> **Comments:**
> **username_1**: Simultaneously cross-posted at https://cs.stackexchange.com/questions/170457/pairwise-partial-equivalence-of-boolean-functions .  

---

## 2 answers

### Answer by username_2 on 2024-11-22. Score: 5 | Accepted answer

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 by username_3 on 2024-11-24. Score: 5

I suggest you try [binary decision diagrams](https://en.wikipedia.org/wiki/Binary_decision_diagram). 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.

> **Comments:**
> **username_2**: While in the same spirit, this answer is actually better than mine since it addresses the OP problem of finding assignments where $b_i=b_j$ while mine is about finding assignments where both are true (I focused on the solution proposed by the OP and not on the core problem). So XORing the data structure is what you need, not the conjunction of course.  

---

