Mathematica Stack Exchange is a question and answer site for users of Mathematica. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|improve this question
    
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
up vote 19 down vote accepted

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

share|improve this answer
4  
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
5  
@DavidZhang members.wolfram.com/adams – Mr.Wizard Jan 10 at 13:50

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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