# Is inverse CNF polynomial?

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$$?

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$$.
• 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. Sep 18, 2019 at 3:13