25
$\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?

Improve this question
$\endgroup$
2
  • $\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
    Commented Jan 9, 2016 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
    Commented Jan 12, 2016 at 18:58

1 Answer 1

Reset to default
28
$\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}}

Improve this answer
$\endgroup$
3
  • 4
    $\begingroup$ Ah, I had no idea SatisfiableQ had a Method option. This should really be documented. $\endgroup$
    – David Zhang
    Commented Jan 10, 2016 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
    Commented Jan 10, 2016 at 11:50
  • 10
    $\begingroup$ @DavidZhang members.wolfram.com/adams $\endgroup$
    – Mr.Wizard
    Commented Jan 10, 2016 at 13:50

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.