Is the following problem in PTIME, or coNP-hard:
Given two Boolean expressions $e_1$ and $e_2$ in variables $x_1,\dots,x_n$, without negation (ie, the expressions are entirely built up via $\wedge$ and $\vee$). Decide whether $e_1 \equiv e_2$, that is they have the same value for all assignments to the variables.
If both expressions would be given in DNF, then the problem is in PTIME since we could first lexicographically order the conjunctive clauses and compare. But bringing an arbitrary expression to DNF can blow up exponentially. A similar argument seems to hold for binary-decision-diagrams.
Obviously, the problem is in coNP.
I was Googling around a fair amount, but couldn't find any answer.
Apologies for the elementary question.
