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

Question

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.

Answer 1

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.

Answer 2

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