1
$\begingroup$

Suppose we are given a CNF formula $F$ with $n$ variables and $m$ clauses. The question is whether we can represent $\lnot F$ as a CNF formula with the number of clauses polynomial in $n$ and $m$?

$\endgroup$
1
$\begingroup$

No, not necessarily.

If $F$ is $(\neg X_1 \lor \neg Y_1) \land \dots \land (\neg X_n \lor \neg Y_n)$, then expressing $\neg F$ in CNF requires exponentially $2^n$ clauses. See, e.g., https://en.wikipedia.org/wiki/Conjunctive_normal_form#Conversion_into_CNF, Which CNF boolean formulas blow up exponentially at conversion to DNF?, and Formulas for which any equivalent CNF formula has exponential length.

However, if you allow introducing additional variables, then you can construct a formula $G$ that is equisatisfiable with $\neg F$ and such that $G$ can be represented in CNF with number of variables and clauses polynomial in $n$ and $m$.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Cool. This example is exactly what I used in my previous question. Can you carry on to show that the "partial question" on that page is impossible? Actually this question arised when I was thinking about that question. $\endgroup$ – Zirui Wang Sep 18 '19 at 2:02
  • $\begingroup$ I think the disjointness of clauses is central to the possibility of polynomial SAT solving. How do you handle that? By disjointness, I mean two clauses differ in their variables. They could have a common part, but I haven't thought of that case yet. When they differ in variables, there will be a lot of interactions in the $n$-dimensional search space, which could lead to exponentiality. $\endgroup$ – Zirui Wang Sep 18 '19 at 3:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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