<p>I found a partial solution. The problem is in L.</p>

<p>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.</p>

<p>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.</p>

<p>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.</p>

<p>So the problem is at least in L. </p>

<hr>

<p>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!</p>

<hr>

<p>EDIT2: there it is, <a href="http://iml.univ-mrs.fr/~bagnol/drafts/mall_bdd.pdf" rel="nofollow">http://iml.univ-mrs.fr/~bagnol/drafts/mall_bdd.pdf</a></p>

<p>So the problem is indeed Logspace-complete.</p>

CC BY-SA 3.0
2015-01-23T09:04:44.373Z
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}$
Denis
CC BY-SA 3.0
2015-01-23T10:19:57.327Z
@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.
Nicolas Perrin
CC BY-SA 3.0
2015-01-23T11:37:04.697Z
@NicolasPerrin Indeed !
Denis
CC BY-SA 3.0
2015-01-23T14:35:33.210Z
@Denis: isn't the idea that a logarithmic number of bits is enough to uniquely identify a path to a leaf, as long as the tree is somewhat balanced?  (However, I don't immediately see what to do about trees that have linear depth, maybe some argument about amortised logarithmic space?)
András Salamon
CC BY-SA 3.0
2015-01-23T14:39:47.777Z
@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.
Denis
CC BY-SA 3.0
2015-01-23T14:42:28.713Z
@Denis: Right, that makes sense.  So L it is.
András Salamon
CC BY-SA 3.0
2015-01-24T10:46:46.183Z
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.
Kaveh
CC BY-SA 3.0
2015-01-24T10:52:19.410Z
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).
Kaveh
CC BY-SA 3.0
2015-01-24T17:22:16.827Z
I have very little intuition on these circuit classes. But I'd be very interested if it is the case. By the way isn't that a classical result then? (equiv of read-once decision trees is in the class [blah])
Marc
CC BY-SA 3.0
2015-01-23T04:43:54.607Z
2015-02-06T19:15:02.207Z
2015-02-06T19:15:02.207Z
Marc
<p>From a ITE formula $\phi$, you can compute polynomially a reduced assignment list to describe all valuations which makes it true.</p>

<p>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.</p>

<p>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&lt;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.</p>

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

CC BY-SA 3.0
2015-01-23T03:00:43.827Z
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
CC BY-SA 3.0
2015-01-23T08:54:24.703Z
Ah yes forgot that, I'm adding a fix hoping it works now.
Denis
CC BY-SA 3.0
2015-01-23T21:11:46.577Z
Don't forget to claim your million $ if it works :)
Marc
CC BY-SA 3.0
2015-01-24T01:01:53.627Z
Yes, apparently I reduced a problem in $L$ to a coNP-complete one, so much for efficency...
Denis
CC BY-SA 3.0
2015-01-23T00:48:45.707Z
2015-01-23T09:02:30.233Z
2015-01-23T09:02:30.233Z
Denis
<p>A read-once decision tree is defined as follows:</p>
<ul>
<li><span class="math-container">$True$</span> and <span class="math-container">$False$</span> are read-once decision trees.</li>
<li>If <span class="math-container">$A$</span> and <span class="math-container">$B$</span> are read-once decision trees and
<span class="math-container">$x$</span> is a variable not occurring in <span class="math-container">$A$</span> and <span class="math-container">$B$</span>,
then <span class="math-container">$(x \land A) \lor (\bar x \land B)$</span> is also a read-once decision tree.</li>
</ul>
<p>What is the complexity of the equivalence problem for read-once decision trees?</p>
<ul>
<li>Input: Two read-once decision trees <span class="math-container">$A$</span> and <span class="math-container">$B$</span>.</li>
<li>Output: Is <span class="math-container">$A \equiv B$</span>?</li>
</ul>
<hr />
<h3>Motivation:</h3>
<p>This problem came up while I was looking at
the proof equivalence problem (permutation of rules) of
a fragment of Linear Logic.</p>

CC BY-SA 3.0
2015-01-23T11:47:33.233Z
Can't you use reduced binary decision diagrams?  Edit: err maybe not, your variables are not ordered...
Sylvain
CC BY-SA 3.0
2015-01-23T23:46:41.677Z
@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
CC BY-SA 3.0
2015-01-24T10:21:03.950Z
@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.)
Kaveh
CC BY-SA 3.0
2015-01-24T18:01:19.190Z
@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
<cc.complexity-theory><lo.logic><decision-trees><boolean-formulas>
What is the complexity of the equivalence problem for read-once decision trees?
Marc
# What is the complexity of the equivalence problem for read-once decision trees?

(Asked by: username_0 on 2015-01-22)

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.

**Tags:** cc.complexity-theory, lo.logic, decision-trees, boolean-formulas
> **Comments:**
> **username_1**: Can't you use reduced binary decision diagrams?  Edit: err maybe not, your variables are not ordered...  
> **username_0**: @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.  
> **username_2**: @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.)  
> **username_0**: @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)  

---

## 2 answers

### Answer by username_0 on 2015-01-23. Score: 5 | Accepted answer

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.

> **Comments:**
> **username_3**: 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}$  
> **username_4**: @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.  
> **username_3**: @NicolasPerrin Indeed !  
> **username_5**: @Denis: isn't the idea that a logarithmic number of bits is enough to uniquely identify a path to a leaf, as long as the tree is somewhat balanced?  (However, I don't immediately see what to do about trees that have linear depth, maybe some argument about amortised logarithmic space?)  
> **username_3**: @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.  
> **username_5**: @Denis: Right, that makes sense.  So L it is.  
> **username_2**: 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.  
> **username_2**: 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).  
> **username_0**: I have very little intuition on these circuit classes. But I'd be very interested if it is the case. By the way isn't that a classical result then? (equiv of read-once decision trees is in the class [blah])  

---

### Answer by username_3 on 2015-01-23. Score: 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

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

> **Comments:**
> **username_0**: 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.  
> **username_3**: Ah yes forgot that, I'm adding a fix hoping it works now.  
> **username_0**: Don't forget to claim your million $ if it works :)  
> **username_3**: Yes, apparently I reduced a problem in $L$ to a coNP-complete one, so much for efficency...  

---

