# Could SAT solvers be significantly more efficient if they allowed for non-CNF formula?

SAT Solvers focus on CNF formulas. For many implications it is much mroe natural to use implications and conjunctions to encode problems, and when converting to CNFs, information is lost, and the solver may need to extra work.

Is it possible that if we would rewrite SAT solvers to solve formulae using conjunctions and implications (and actually use that information, not just rewrite to CNF first), that this would open up significant efficiencies for problems that are naturally encoded using conjunctions and implications?

• Any conjunction-and-implications formula in $n$ variables can be rewritten in CNF form in $n$ variables, so no.
– user16034
Sep 7, 2023 at 9:54

First, I want to note that many implications are already natively supported. The implication $$u \implies x$$ is equivalent to $$\neg u \lor x$$, which is a CNF clause. Similarly, the implication $$(u \land v \land w) \implies x$$ is equivalent to $$\neg u \lor \neg v \lor \neg w \lor x$$, which is also a CNF clause. So many implications (specifically, all Horn clauses) are already in CNF form, and thus no modification to the SAT solver is needed. Also, while implications like $$(u \lor v) \implies x$$ are not directly in CNF form, they are equivalent to $$(u \implies x) \land (v \implies x)$$, which in turn is equivalent to $$(\neg u \lor x) \land (\neg v \lor x)$$, which is a conjunction of two CNF clauses. So this type of implication is also natively supported.