3
$\begingroup$

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?

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

1 Answer 1

2
$\begingroup$

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.

$\endgroup$

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.