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, 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!

  • 2
    $\begingroup$ Equivalence of monotone formulas is well known to be coNP-complete. I’m not sure whether this holds already for CNF. $\endgroup$ Dec 12, 2019 at 18:26
  • $\begingroup$ See the references on page 4 of webis.de/downloads/publications/papers/hagen_2008b.pdf . $\endgroup$ Dec 12, 2019 at 18:28
  • 2
    $\begingroup$ 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. $\endgroup$ Dec 12, 2019 at 19:20
  • 3
    $\begingroup$ Check out the following paper: arxiv.org/abs/cs/0202036 It looks like your problem is in P. $\endgroup$ Dec 12, 2019 at 19:32
  • 2
    $\begingroup$ 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. $\endgroup$ Dec 12, 2019 at 20:35

1 Answer 1


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


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

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

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

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

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

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

  • $\begingroup$ I'd add an additional upvote if possible for the interesting references! $\endgroup$ Dec 14, 2019 at 0:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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