<p>Note that formulas using <span class="math-container">$\land$</span> and <span class="math-container">$\lor$</span> gates (and possibly the constants <span class="math-container">$0$</span> and <span class="math-container">$1$</span>) are known as <em>monotone</em>.</p>

<p>The complexity of monotone formula equivalence depends on how complex formulas are allowed. Let me start with the related problem of <em>implication</em> (entailment) between two formulas <span class="math-container">$\phi\vdash\psi$</span>, which is easier to classify. Note that <span class="math-container">$\phi$</span> and <span class="math-container">$\psi$</span> are equivalent iff <span class="math-container">$\phi\vdash\psi$</span> and <span class="math-container">$\psi\vdash\phi$</span>.</p>

<p>Given monotone formulas <span class="math-container">$\phi$</span> and <span class="math-container">$\psi$</span>, the problem of determining whether <span class="math-container">$\phi\vdash\psi$</span> is</p>

<ul>
<li><p>in <strong>P</strong> for <span class="math-container">$\psi$</span> a CNF (even non-monotone). Indeed, we have <span class="math-container">$\phi\vdash\bigwedge_i\psi_i$</span> iff <span class="math-container">$\forall i\,(\phi\vdash\psi_i)$</span>, and if <span class="math-container">$\psi_i$</span> is a clause, and <span class="math-container">$e_i$</span> the corresponding assignment that falsifies <span class="math-container">$\psi_i$</span> and makes all variables outside <span class="math-container">$\psi_i$</span> true, then
<span class="math-container">$$\phi\vdash\psi_i\iff e_i(\phi)=0.$$</span>
For the right-to-left direction: if <span class="math-container">$e_i(\phi)=0$</span>, and <span class="math-container">$e$</span> is any assignment such that <span class="math-container">$e(\psi_i)=0$</span>, then <span class="math-container">$e\le e_i$</span>, hence <span class="math-container">$e(\phi)=0$</span> using the monotonicity of <span class="math-container">$\phi$</span>.</p></li>
<li><p>in <strong>P</strong> for <span class="math-container">$\phi$</span> a DNF (possibly non-monotone), by a dual argument.</p></li>
<li><p><strong>coNP</strong>-complete for <span class="math-container">$\phi$</span> a 2-CNF and <span class="math-container">$\psi$</span> a 3-DNF (or dually: <span class="math-container">$\phi$</span> a 3-CNF and <span class="math-container">$\psi$</span> a 2-DNF), and <em>a fortiori</em> for any larger classes of formulas. Indeed, it is <strong>coNP</strong>-hard to check if a given 3-DNF is valid; we can write (in polynomial time) any 3-DNF in the form <span class="math-container">$\psi(\vec x,\neg\vec x)$</span> where <span class="math-container">$\psi$</span> is a monotone 3-DNF, and then
<span class="math-container">$$\vdash\psi(\vec x,\neg\vec x)\iff\bigwedge_i(x_i\lor y_i)\vdash\psi(\vec x,\vec y).$$</span>
As above, the left-to-right direction follows from the monotonicity of <span class="math-container">$\psi$</span>.</p></li>
</ul>

<p>Now, back to equivalence. On the one hand, we have
<span class="math-container">$$\phi\equiv\psi\iff\phi\vdash\psi\text{ and }\psi\vdash\phi;$$</span>
on the other hand,
<span class="math-container">$$\phi\vdash\psi\iff \phi\equiv(\phi\land\psi)\iff\psi\equiv(\phi\lor\psi).$$</span>
Thus, we see that for monotone <span class="math-container">$\phi$</span> and <span class="math-container">$\psi$</span>, the problem of determining if <span class="math-container">$\phi\equiv\psi$</span> is</p>

<ul>
<li><p>in <strong>P</strong> for <span class="math-container">$\phi$</span> and <span class="math-container">$\psi$</span> CNF.</p></li>
<li><p>in <strong>P</strong> for <span class="math-container">$\phi$</span> and <span class="math-container">$\psi$</span> DNF.</p></li>
<li><p><strong>coNP</strong>-complete for general monotone <span class="math-container">$\phi$</span> and <span class="math-container">$\psi$</span>. It is enough to take <span class="math-container">$\phi$</span> a CNF, and <span class="math-container">$\psi$</span> a conjunction of a CNF and a DNF (which means <span class="math-container">$\psi$</span> can be written as a depth-3 formula with either <span class="math-container">$\bigwedge$</span> or <span class="math-container">$\bigvee$</span> as the top connective). Dually, it is enough to take <span class="math-container">$\phi$</span> a DNF, and <span class="math-container">$\psi$</span> a disjunction of a CNF and a DNF (whence again a depth-3 formula with either <span class="math-container">$\bigwedge$</span> or <span class="math-container">$\bigvee$</span> on top).</p></li>
</ul>

<p>The only case left is the complexity of equivalence of a monotone CNF to a monotone DNF. This problem is <em>interesting</em>. As I learned in [4], it was proved to be solvable in quasipolynomial time <span class="math-container">$O(n^{\log n})$</span> by [3], and in <strong>coNP</strong> with only <span class="math-container">$O((\log n)^2)$</span> nondeterministic bits by [2,5]. Furthermore, when one of the formulas has bounded width, the problem is in <strong>P</strong> by [1,6], and even in <strong>L</strong> by [4].</p>

<p><strong>References:</strong></p>

<p>[1] T. Eiter, G. Gottlob: <em>Identifying the minimal transversals of a hypergraph and related problems</em>, SIAM Journal on Computing 24 (1995), no. 6, pp. 1278–1304, doi: <a href="https://doi.org/10.1137/S0097539793250299" rel="noreferrer">10.1137/S0097539793250299</a>.</p>

<p>[2] T. Eiter, G. Gottlob, K. Makino: <em>New results on monotone dualization and generating hypergraph transversals</em>, SIAM Journal on Computing 32 (2003), no. 2, pp. 514–537, doi: <a href="https://doi.org/10.1137/S009753970240639X" rel="noreferrer">10.1137/S009753970240639X</a>.</p>

<p>[3] M. L. Fredman, L. Khachiyan: <em>On the complexity of dualization of monotone disjunctive normal forms</em>, Journal of Algorithms 21 (1996), no. 3, pp. 618–628, doi: <a href="https://doi.org/10.1006/jagm.1996.0062" rel="noreferrer">10.1006/jagm.1996.0062</a>.</p>

<p>[4] J. Goldsmith, M. Hagen, M. Mundhenk: <em>Complexity of DNF minimization and isomorphism testing for monotone formulas</em>, Information and Computation
206 (2008), no. 6, pp. 760–775, doi: <a href="https://doi.org/10.1016/j.ic.2008.03.002" rel="noreferrer">10.1016/j.ic.2008.03.002</a>.</p>

<p>[5] D. J. Kavvadias, E. C. Stavropoulos: <em>Monotone Boolean dualization is in <span class="math-container">$\mathrm{coNP}[\log^2n]$</span></em>, Information Processing Letters 85 (2003), no. 1, pp. 1–6, doi: <a href="https://doi.org/10.1016/S0020-0190(02)00346-0" rel="noreferrer">doi.org/10.1016/S0020-0190(02)00346-0</a>.</p>

<p>[6] N. Mishra, L. Pitt: <em>Generating all maximal independent sets of bounded-degree hypergraphs</em>. In: Proceedings of the Tenth Annual Conference on Computational Learning Theory (COLT 1997), 1997, pp. 211–217, doi: <a href="https://doi.org/10.1145/267460.267500" rel="noreferrer">10.1145/267460.267500</a>.</p>

CC BY-SA 4.0
2019-12-14T00:16:25.853Z
I'd add an additional upvote if possible for the interesting references!
wanderingmathematician
CC BY-SA 4.0
2019-12-13T16:06:47.387Z
2019-12-13T16:06:47.387Z
Emil Jeřábek
<p>Suppose I have two boolean formulae (propositions) <span class="math-container">$P_1$</span>, and <span class="math-container">$P_2$</span> (can be assumed to be in CNF) over the same variables and such that there are no "NOT" symbols used.  I.e. only conjunction and disjunction are used but not negation.  Then what is the complexity of checking if <span class="math-container">$P_1$</span> and <span class="math-container">$P_2$</span> are equivalent (they are equivalent iff they agree on all inputs)?</p>

<p>By <a href="https://stackoverflow.com/questions/37185366/two-boolean-expressions-equivalence-co-np">This answer</a>, I know that if negation is allowed, this problem is co-NP complete.  It is also easy to see that if I simply wanted to check satisifiability for either proposition when negation is disallowed, I would have a linear time algorithm by simply setting all variables to true and checking if the proposition is true.</p>

<p>However, I am not sure what the complexity of checking equivalence in this case would be.  I could say that the two propositions are equivalent iff (<span class="math-container">$P_1 \wedge \neg P_2$</span>) and (<span class="math-container">$P_2 \wedge \neg P_1$</span>) are both unsatisfiable, but I can't use the linear time SAT algorithm above because now I have negation in these new propositions.</p>

<p>Can anyone help me figure out what the complexity of this problem is?</p>

<p>Much obliged!</p>

CC BY-SA 4.0
2019-12-12T18:26:34.740Z
Equivalence of monotone formulas is well known to be coNP-complete. I’m not sure whether this holds already for CNF.
Emil Jeřábek
CC BY-SA 4.0
2019-12-12T18:28:13.683Z
See the references on page 4 of https://webis.de/downloads/publications/papers/hagen_2008b.pdf .
Emil Jeřábek
CC BY-SA 4.0
2019-12-12T19:20:02.890Z
Oh, actually, equivalence of monotone CNF is decidable in polynomial time: if $C_i$ and $D_j$ are monotone clauses, then $\bigwedge_iC_i\equiv\bigwedge_jD_j$ if and only if $\forall j\,\exists i\, C_i\subseteq D_j$ and vice versa.
Emil Jeřábek
CC BY-SA 4.0
2019-12-12T19:32:41.497Z
Check out the following paper: https://arxiv.org/abs/cs/0202036 It looks like your problem is in P.
Gustav Nordh
CC BY-SA 4.0
2019-12-12T20:15:32.753Z
@GustavNordh Damn, you got my hopes up!  The paper you sent is great, although just above theorem 6 it actually says that my problem is still coNP-complete :(
wanderingmathematician
CC BY-SA 4.0
2019-12-12T20:20:06.523Z
@GustavNordh Actually now I'm confused by that statement... With no negations allowed, my formulas (constraints, using the terminology from the paper) should be anti-Horn, right?  Hence Schaefer hence the problem should be P.  Yet just above theorem 6 it says that arbitrary boolean formulas only involving AND and OR but excluding NOT is still coNP complete.  What am I missing?
wanderingmathematician
CC BY-SA 4.0
2019-12-12T20:35:27.040Z
In order to apply the theorem, you need to fix a finite set of contraints, and consider sets of instances of such constraints. What you get in this way are nowhere near all monotone formulas, but only monotone formulas that can be written as conjunctions of clauses of bounded width. This is an even more restrictive class of formulas than monotone CNF, and as I already pointed out, equivalence of monotone CNF is polynomial time. In order to get coNP-completeness, you need more complex monotone formulas.
Emil Jeřábek
CC BY-SA 4.0
2019-12-12T20:56:15.070Z
@EmilJeřábeksupportsMonica Ah, I see!  I apologize--I wasn't familiar with the term monotone and didn't realize it was equivalent to the condition I had specified.  Thanks!  Would you mind pointing out where you found the proof of the polynomial time claim from your third comment?  I would be happy to accept that as an answer!
wanderingmathematician
CC BY-SA 4.0
2019-12-13T07:56:17.097Z
The proof is quite simple, I found it in my head.
Emil Jeřábek
<cc.complexity-theory><lo.logic><sat><boolean-functions>
What is the complexity of checking equivalence of two boolean formulae without NOT symbol?
wanderingmathematician
# What is the complexity of checking equivalence of two boolean formulae without NOT symbol?

(Asked by: username_0 on 2019-12-12)

Suppose I have two boolean formulae (propositions) $P\_1$, and $P\_2$ (can be assumed to be in CNF) over the same variables and such that there are no "NOT" symbols used. I.e. only conjunction and disjunction are used but not negation. Then what is the complexity of checking if $P\_1$ and $P\_2$ are equivalent (they are equivalent iff they agree on all inputs)?

By [This answer](https://stackoverflow.com/questions/37185366/two-boolean-expressions-equivalence-co-np), I know that if negation is allowed, this problem is co-NP complete. It is also easy to see that if I simply wanted to check satisifiability for either proposition when negation is disallowed, I would have a linear time algorithm by simply setting all variables to true and checking if the proposition is true.

However, I am not sure what the complexity of checking equivalence in this case would be. I could say that the two propositions are equivalent iff ($P\_1 \wedge \neg P\_2$) and ($P\_2 \wedge \neg P\_1$) are both unsatisfiable, but I can't use the linear time SAT algorithm above because now I have negation in these new propositions.

Can anyone help me figure out what the complexity of this problem is?

Much obliged!

**Tags:** cc.complexity-theory, lo.logic, sat, boolean-functions
> **Comments:**
> **username_1**: Equivalence of monotone formulas is well known to be coNP-complete. I’m not sure whether this holds already for CNF.  
> **username_1**: See the references on page 4 of https://webis.de/downloads/publications/papers/hagen_2008b.pdf .  
> **username_1**: Oh, actually, equivalence of monotone CNF is decidable in polynomial time: if $C_i$ and $D_j$ are monotone clauses, then $\bigwedge_iC_i\equiv\bigwedge_jD_j$ if and only if $\forall j\,\exists i\, C_i\subseteq D_j$ and vice versa.  
> **username_2**: Check out the following paper: https://arxiv.org/abs/cs/0202036 It looks like your problem is in P.  
> **username_0**: @GustavNordh Damn, you got my hopes up!  The paper you sent is great, although just above theorem 6 it actually says that my problem is still coNP-complete :(  
> **username_0**: @GustavNordh Actually now I'm confused by that statement... With no negations allowed, my formulas (constraints, using the terminology from the paper) should be anti-Horn, right?  Hence Schaefer hence the problem should be P.  Yet just above theorem 6 it says that arbitrary boolean formulas only involving AND and OR but excluding NOT is still coNP complete.  What am I missing?  
> **username_1**: In order to apply the theorem, you need to fix a finite set of contraints, and consider sets of instances of such constraints. What you get in this way are nowhere near all monotone formulas, but only monotone formulas that can be written as conjunctions of clauses of bounded width. This is an even more restrictive class of formulas than monotone CNF, and as I already pointed out, equivalence of monotone CNF is polynomial time. In order to get coNP-completeness, you need more complex monotone formulas.  
> **username_0**: @EmilJeřábeksupportsMonica Ah, I see!  I apologize--I wasn't familiar with the term monotone and didn't realize it was equivalent to the condition I had specified.  Thanks!  Would you mind pointing out where you found the proof of the polynomial time claim from your third comment?  I would be happy to accept that as an answer!  
> **username_1**: The proof is quite simple, I found it in my head.  

---

## 1 answers

### Answer by username_1 on 2019-12-13. Score: 15 | Accepted answer

Note that formulas using $\land$ and $\lor$ gates (and possibly the constants $0$ and $1$) are known as *monotone*.

The complexity of monotone formula equivalence depends on how complex formulas are allowed. Let me start with the related problem of *implication* (entailment) between two formulas $\phi\vdash\psi$, which is easier to classify. Note that $\phi$ and $\psi$ are equivalent iff $\phi\vdash\psi$ and $\psi\vdash\phi$.

Given monotone formulas $\phi$ and $\psi$, the problem of determining whether $\phi\vdash\psi$ is

* in **P** for $\psi$ a CNF (even non-monotone). Indeed, we have $\phi\vdash\bigwedge\_i\psi\_i$ iff $\forall i\,(\phi\vdash\psi\_i)$, and if $\psi\_i$ is a clause, and $e\_i$ the corresponding assignment that falsifies $\psi\_i$ and makes all variables outside $\psi\_i$ true, then
  $$\phi\vdash\psi\_i\iff e\_i(\phi)=0.$$
  For the right-to-left direction: if $e\_i(\phi)=0$, and $e$ is any assignment such that $e(\psi\_i)=0$, then $e\le e\_i$, hence $e(\phi)=0$ using the monotonicity of $\phi$.
* in **P** for $\phi$ a DNF (possibly non-monotone), by a dual argument.
* **coNP**-complete for $\phi$ a 2-CNF and $\psi$ a 3-DNF (or dually: $\phi$ a 3-CNF and $\psi$ a 2-DNF), and *a fortiori* for any larger classes of formulas. Indeed, it is **coNP**-hard to check if a given 3-DNF is valid; we can write (in polynomial time) any 3-DNF in the form $\psi(\vec x,\neg\vec x)$ where $\psi$ is a monotone 3-DNF, and then
  $$\vdash\psi(\vec x,\neg\vec x)\iff\bigwedge\_i(x\_i\lor y\_i)\vdash\psi(\vec x,\vec y).$$
  As above, the left-to-right direction follows from the monotonicity of $\psi$.

Now, back to equivalence. On the one hand, we have
$$\phi\equiv\psi\iff\phi\vdash\psi\text{ and }\psi\vdash\phi;$$
on the other hand,
$$\phi\vdash\psi\iff \phi\equiv(\phi\land\psi)\iff\psi\equiv(\phi\lor\psi).$$
Thus, we see that for monotone $\phi$ and $\psi$, the problem of determining if $\phi\equiv\psi$ is

* in **P** for $\phi$ and $\psi$ CNF.
* in **P** for $\phi$ and $\psi$ DNF.
* **coNP**-complete for general monotone $\phi$ and $\psi$. It is enough to take $\phi$ a CNF, and $\psi$ a conjunction of a CNF and a DNF (which means $\psi$ can be written as a depth-3 formula with either $\bigwedge$ or $\bigvee$ as the top connective). Dually, it is enough to take $\phi$ a DNF, and $\psi$ a disjunction of a CNF and a DNF (whence again a depth-3 formula with either $\bigwedge$ or $\bigvee$ on top).

The only case left is the complexity of equivalence of a monotone CNF to a monotone DNF. This problem is *interesting*. As I learned in [4], it was proved to be solvable in quasipolynomial time $O(n^{\log n})$ by [3], and in **coNP** with only $O((\log n)^2)$ nondeterministic bits by [2,5]. Furthermore, when one of the formulas has bounded width, the problem is in **P** by [1,6], and even in **L** by [4].

**References:**

[1] T. Eiter, G. Gottlob: *Identifying the minimal transversals of a hypergraph and related problems*, SIAM Journal on Computing 24 (1995), no. 6, pp. 1278–1304, doi: [10.1137/S0097539793250299](https://doi.org/10.1137/S0097539793250299).

[2] T. Eiter, G. Gottlob, K. Makino: *New results on monotone dualization and generating hypergraph transversals*, SIAM Journal on Computing 32 (2003), no. 2, pp. 514–537, doi: [10.1137/S009753970240639X](https://doi.org/10.1137/S009753970240639X).

[3] M. L. Fredman, L. Khachiyan: *On the complexity of dualization of monotone disjunctive normal forms*, Journal of Algorithms 21 (1996), no. 3, pp. 618–628, doi: [10.1006/jagm.1996.0062](https://doi.org/10.1006/jagm.1996.0062).

[4] J. Goldsmith, M. Hagen, M. Mundhenk: *Complexity of DNF minimization and isomorphism testing for monotone formulas*, Information and Computation
206 (2008), no. 6, pp. 760–775, doi: [10.1016/j.ic.2008.03.002](https://doi.org/10.1016/j.ic.2008.03.002).

[5] D. J. Kavvadias, E. C. Stavropoulos: *Monotone Boolean dualization is in $\mathrm{coNP}[\log^2n]$*, Information Processing Letters 85 (2003), no. 1, pp. 1–6, doi: [doi.org/10.1016/S0020-0190(02)00346-0](https://doi.org/10.1016/S0020-0190(02)00346-0).

[6] N. Mishra, L. Pitt: *Generating all maximal independent sets of bounded-degree hypergraphs*. In: Proceedings of the Tenth Annual Conference on Computational Learning Theory (COLT 1997), 1997, pp. 211–217, doi: [10.1145/267460.267500](https://doi.org/10.1145/267460.267500).

> **Comments:**
> **username_0**: I'd add an additional upvote if possible for the interesting references!  

---

