What is the complexity of the equivalence problem for read-once decision trees?

A read-once decision tree is defined as follows:

• $$True$$ and $$False$$ are read-once decision trees.
• If $$A$$ and $$B$$ are read-once decision trees and $$x$$ is a variable not occurring in $$A$$ and $$B$$, then $$(x \land A) \lor (\bar x \land B)$$ is also a read-once decision tree.

What is the complexity of the equivalence problem for read-once decision trees?

• Input: Two read-once decision trees $$A$$ and $$B$$.
• Output: Is $$A \equiv B$$?

Motivation:

This problem came up while I was looking at the proof equivalence problem (permutation of rules) of a fragment of Linear Logic.

• Can't you use reduced binary decision diagrams? Edit: err maybe not, your variables are not ordered... Jan 23, 2015 at 11:47
• @Kaveh Nope, it occurs in proof theory: I am looking at the proof equivalence problem (permutation of rules) of a fragment of Linear Logic. Boils down to this boolean problem. As I am no specialist, I figured I'd ask if ever this was a well know/easy question. Hence, yeah I made up the name because I don't know any better.
– Marc
Jan 23, 2015 at 23:46
• @Marc, it is generally a good idea to explain why you are interested in a problem. I edited the question. Please have a look to make sure it is fine. (Also removing my previous comments since they are not needed anymore.) Jan 24, 2015 at 10:21
• @Kaveh Yeah, sorry about that. I edited your reformulation to make it closer to my original argument (I couldn't figure immediately if yours was OK so it seemed easier to do this)
– Marc
Jan 24, 2015 at 18:01

I found a partial solution. The problem is in L.

The negation of $A \leftrightarrow B$ is equivalent to $(\bar A \land B) \lor (A \land \bar{B})$ which is equivalent to $False$ iff both $(\bar A \land B)$ and $(A \land \bar{B})$ are.

The read-once decision tree for $\bar{A}$ can be obtained from the read-once decision tree for $A$ by switching $True$ and $False$ in $A$. This can be done in log space.

To check if $\bar A \land B$ is equivlent to $False$ (and similarly for ${A} \land \bar{B}$) we run through all the pairs of $True$ leaves, one from each tree, and check if they are compatible (that is there is no $x$ on one of the paths and $\bar x$ on the other). It is equivalent to $False$ iff we find no compatible pair. This can be done in log space.

So the problem is at least in L.

EDIT: I have some ideas to prove this to be L-complete, under $AC_0$ reduction probably. But I'd need to check the details and it won't fit in here. I'll post a link to the article I am writing if it all works out!

EDIT2: there it is, http://iml.univ-mrs.fr/~bagnol/drafts/mall_bdd.pdf

So the problem is indeed Logspace-complete.

• how do you get this negation ? The negation of $x.A+\overline{x}.B$ should be $(\overline{x}+\overline{A}).(x+\overline{B})$, i.e. $x.\overline{A}+\overline{x}.\overline{B}+\overline{A}.\overline{B}$ Jan 23, 2015 at 9:04
• @Denis: I believe this was a typo, your formula simplifies to $x.\bar A+\bar x.\bar B$, so indeed the negation is computed by flipping the 0 and 1 at the leaves. Jan 23, 2015 at 10:19
• @AndrásSalamon no actually the number of leaves is linear in the size of the formula, so you need a logarithmic number of bits to identify them, no matter how the tree is balanced. Then you just check that there is a problematic variable (one with $x$ on a path and $\overline{x}$ on the other) for each pair of $1$. I thought there was a problem because you needed to guess the problematic variable for each pair, but actually you can just try them all one after the other, it stays in $L$ because the number of variables is linear. Jan 23, 2015 at 14:39
• An easier way to state this is: Each path is a min-term or max-term depending its leaf's label. We check if they have the same min-terms. We can enumerate the min-terms in log space and checking if two min-terms are the same is in log space. Jan 24, 2015 at 10:46
• It seems to me this can actually be done in $NC^1$ (or even $AC^0$) if you use a representation of the trees such that you can check if a node is an ancestors of another one in $AC^0$ (e.g. something like extended connection language for the circuit). Jan 24, 2015 at 10:52

From a ITE formula $\phi$, you can compute polynomially a reduced assignment list to describe all valuations which makes it true.

To do that, just look at your formula as a tree with nodes labeled by variables and leaves by $0$ and $1$. Left branches are the "then" part setting the variable to true and right branches are the "else" part setting it to false. Each branch leading to a leave $1$ will be labeled by a set of partial variables assignement, for instance $\{x,\overline{y},z\}$. Computing the list of all these sets from your formula is polynomial. You can then compute a normal form of this list by removing a set if it is contained in an other one, and merging sets that differ on a variable: if $\{x,\overline{y},z\}$ and $\{x,y,z\}$ are in your list, you remove them and add $\{x,z\}$, meaning that it works no matter the value of $y$. However, if you have $\{x,\overline{y},z,t\}$ and $\{x,y,z\}$, you cannot merge them and keep them like this. You apply these rules until you stabilize, once again this procedure is polynomial.

Finally, choose an arbitrary ordering on variables $\{x_1,\dots,x_n\}$, and call $i$ the weight of $x_i$. The weight of a list is the sum of all weights appearing in it (with multiplicites). Apply "rotations" everytime it is possible, in order to minimize the total weight of your normal form. A rotation changes $\{\vec x,x_i,x_j\},\{\vec x,\overline{x_j}\}$ to $\{\vec x,x_i\},\{\vec x,\overline{x_i},\overline{x_j}\}$ with $i<j$ ($\vec x$ is a list, and $x_i$ and $x_j$ can also be negated variables). We can see that it makes the total weight decrease by $j-i$. Hopefully now the normal form is unique, I'll try a formal proof later.

Then, two formulas are equivalent iff they have the same normal form list of assignments. So your problem seems to be in $P$.

• Hi, thanks for your answer, the first part with trees and such is indeed a good way to look at the problem. But the second part does not work: normal forms are not unique, eg. $x,y,z$ - $x,\bar y,z$ - $x,y,\bar z$. There might be a specific thing about ITE formulas that make it work though. But as such it would solve the equivalence of any sum of monomials, which is coNP complete, I believe.
– Marc
Jan 23, 2015 at 3:00
• Ah yes forgot that, I'm adding a fix hoping it works now. Jan 23, 2015 at 8:54
• Don't forget to claim your million $if it works :) – Marc Jan 23, 2015 at 21:11 • Yes, apparently I reduced a problem in$L\$ to a coNP-complete one, so much for efficency... Jan 24, 2015 at 1:01