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?
SatisfiabilityCountis doing a minimization first, e.g., try
SatisfiableQ[BooleanMinimize[bigExpr]]- times are comparable in a quick test here. $\endgroup$