patternMinor
Could SAT solvers be significantly more efficient if they allowed for non-CNF formula?
Viewed 0 times
satallowedsolversnonmoreefficientcouldcnfforsignificantly
Problem
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?
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?
Solution
That's a natural idea. However, to the best of my knowledge, despite attempts, no one has succeeded in making such an approach do better than just converting to CNF and using an existing SAT solver.
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.
Second, I want to note that no information is lost.
Third, a lot of engineering has gone into SAT solvers, with sophisticated methods, like 2 watched literals, conflict analysis, clause learning, backjumping, and more. It is easier and simpler to implement these methods when every clause is in CNF. If you had multiple forms of clauses, then implementing these methods would be more complicated and harder to maintain. Also it would likely introduce a constant-factor slowdown to have to handle all of these cases. So any speedup from native support for alternative clause formats might be outweighed by the slowdown from code that has to check all of these cases. From an engineering perspective, it makes sense to have a simple API and internal representation of the formula.
I'm not saying there is a fundamental barrier to your idea. I'm saying that there are engineering tradeoffs, and so far as I know, to date the engineering tradeoffs don't seem to favor the approach you identify. That could always change as new methods are discovered.
The only case I know of where extending a SAT solver to support additional clause formats has been successful is CryptoSat/CryptoMiniSat, which contains specialized support for XORs.
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.
Second, I want to note that no information is lost.
Third, a lot of engineering has gone into SAT solvers, with sophisticated methods, like 2 watched literals, conflict analysis, clause learning, backjumping, and more. It is easier and simpler to implement these methods when every clause is in CNF. If you had multiple forms of clauses, then implementing these methods would be more complicated and harder to maintain. Also it would likely introduce a constant-factor slowdown to have to handle all of these cases. So any speedup from native support for alternative clause formats might be outweighed by the slowdown from code that has to check all of these cases. From an engineering perspective, it makes sense to have a simple API and internal representation of the formula.
I'm not saying there is a fundamental barrier to your idea. I'm saying that there are engineering tradeoffs, and so far as I know, to date the engineering tradeoffs don't seem to favor the approach you identify. That could always change as new methods are discovered.
The only case I know of where extending a SAT solver to support additional clause formats has been successful is CryptoSat/CryptoMiniSat, which contains specialized support for XORs.
Context
StackExchange Computer Science Q#161909, answer score: 2
Revisions (0)
No revisions yet.