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$?


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

  • $\begingroup$ Can't you use reduced binary decision diagrams? Edit: err maybe not, your variables are not ordered... $\endgroup$ – Sylvain Jan 23 '15 at 11:47
  • $\begingroup$ @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. $\endgroup$ – Marc Jan 23 '15 at 23:46
  • 1
    $\begingroup$ @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.) $\endgroup$ – Kaveh Jan 24 '15 at 10:21
  • $\begingroup$ @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) $\endgroup$ – Marc Jan 24 '15 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.

  • $\begingroup$ 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}$ $\endgroup$ – Denis Jan 23 '15 at 9:04
  • 1
    $\begingroup$ @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. $\endgroup$ – Nicolas Perrin Jan 23 '15 at 10:19
  • 1
    $\begingroup$ @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. $\endgroup$ – Denis Jan 23 '15 at 14:39
  • 1
    $\begingroup$ 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. $\endgroup$ – Kaveh Jan 24 '15 at 10:46
  • 2
    $\begingroup$ 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). $\endgroup$ – Kaveh Jan 24 '15 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$.

  • 1
    $\begingroup$ 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. $\endgroup$ – Marc Jan 23 '15 at 3:00
  • $\begingroup$ Ah yes forgot that, I'm adding a fix hoping it works now. $\endgroup$ – Denis Jan 23 '15 at 8:54
  • $\begingroup$ Don't forget to claim your million $ if it works :) $\endgroup$ – Marc Jan 23 '15 at 21:11
  • $\begingroup$ Yes, apparently I reduced a problem in $L$ to a coNP-complete one, so much for efficency... $\endgroup$ – Denis Jan 24 '15 at 1:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.