# Why is SatisfiabilityCount faster than SatisfiableQ?

Consider the following (large) Boolean expression, which arose in a SAT problem. (The expression is not satisfiable.)

bigExpr = Import["http://pastebin.com/raw/gEgGQ26S"];

On my system (Mathematica 10.3 on Windows 10), I observed the following strange behavior: SatisfiableQ[bigExpr, BooleanVariables@bigExpr] takes 4.53883 seconds to run, while SatisfiabilityCount[bigExpr, BooleanVariables@bigExpr] takes only 0.00588 seconds.

How can it be the case that SatisfiableQ, which only checks for the existence of a satisfying assignment, takes three orders of magnitude more time than SatisfiabilityCount, which counts them?

-
I'd venture SatisfiabilityCount is doing a minimization first, e.g., try SatisfiableQ[BooleanMinimize[bigExpr]] - times are comparable in a quick test here. – ciao Jan 9 at 23:03
Just for the record I've had related - unexplained behavior - experience with some of the Mathematica machine learning functions. Mathematica Support pointed me at some undocumented arguments that enabled me to make sense out of behavior on some "edge" inputs. In summary, Support was very helpful, documentation not so much. – Mark Samuel Tuttle Jan 12 at 18:58

SatisfiableQ has three methods:

• "BDD": converts the expression to a BDD (binary decision diagram),
• "SAT": uses the Minisat library,
• "TREE": a branch-and-bound method based on the expression tree.

SatisfiabilityCount counts instances by converting the expression to a BDD, so its timing should be close to SatisfiableQ with the "BDD" method (counting instances once we have a BDD is fast).

Unfortunately, for this example the automatic method choice heuristic picks the worst method.

Timing[SatisfiableQ[bigExpr, BooleanVariables[bigExpr], Method->#]]&
/@ {Automatic, "BDD", "SAT", "TREE"}

{{3.41648, False}, {0.021996, False}, {0.004, False}, {3.47947, False}}

-
Ah, I had no idea SatisfiableQ had a Method option. This should really be documented. – David Zhang Jan 10 at 2:53
Actually, how do you know that Method -> "SAT" calls the MiniSAT library? I can't find any reference to this fact. – David Zhang Jan 10 at 11:50
@DavidZhang members.wolfram.com/adams – Mr.Wizard Jan 10 at 13:50