23
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ I'd venture SatisfiabilityCount is doing a minimization first, e.g., try SatisfiableQ[BooleanMinimize[bigExpr]] - times are comparable in a quick test here. $\endgroup$ – ciao Jan 9 '16 at 23:03
  • 1
    $\begingroup$ 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. $\endgroup$ – Mark Samuel Tuttle Jan 12 '16 at 18:58
26
$\begingroup$

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}}

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.