Well long story short, the hunt continues but a likely reason is the lack of impact that the simple clause learning scheme actually has. Monitoring the clauses that cause unit propagation (a measure of how useful a clause is) reveals that the learned clauses aren't actually ever being used -- big-time bummer. It's because of this, I've disabled the conflict analysis in the latest version.
But results are still be be had. First off, how much better are we than the original DPLL solver, and how bad does the clause learning actually hurt? Well the answers are (roughly) pretty good, and not much ;). Here's a graph plotting the run-time for the three approaches (-CA means clause learning was disabled):
Note that the y-axis is on a log scale, so the differences are actually more drastic than they appear. Take-away: the new sat-solver is doing great, and the clause learning doesn't hurt that much...just doesn't help like we'd expect.
Next up is the impact of watch literals. I'll have a blog post in a day or two for the final installment of "what goes into a SAT solver", and the focus will be on watch literals. The introduction of this data structure hack heralded in a wave of killer SAT solvers, and they helped out here too. The following is a comparison (with clause learning disabled) between using watch literals and not using them:
Oh, and it should be noted that when points don't exist, it's because the solver just couldn't handle it in a reasonable amount of time.
So in the interest of actually letting SymPy users see these enhancements, I'm going to wrap up this week with that final post, and post-pone the clause learning investigation until more time is available. Next up is investigating how a truth maintenance system can be used to smartly cache queries to the assumption framework. If we can avoid repeated SAT queries (no matter how beefy the solver is), that's a win.
One final note, there will likely be an incorporation of an industrial SAT-solver interface for those who really want the power. This will be through the Numberjack Library, and be optional if you happen to have it installed. The start of it is in this branch, but we'll need to wait until the next version of Numberjack is released due to limitations it currently has.
That's all for now. Cheers.


















