HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

Best improvements to do to the DPLL SAT algorithm

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
satthebestalgorithmimprovementsdpll

Problem

As part of a college class, I'm asked to improve the performance of a basic DPLL sat solver. I'm already provided a basic, slow working version (essentially the DPLL algorithm; furthermore, to select the next variable, it just loops an array and gets the next unused one). I have been reading papers on ways to improve it, but I'm a bit overwhelmed by the amount of optimizations one can do. I'm not looking to make an extremely efficient solver; just something that works better than a plain basic DPLL one. I have read about 2WL, VSIDS, and a handful more. Which optimizations will give me the most performance without overcomplicating things? The input with the most variables that I have to solve is of the order of 300, with 1500 clauses, if that is of any interest.

I apologize if something similar has been asked before, but I haven't found anything. I would appreciate any other tips if you guys have. Thank you.

Solution

The most improvement with the least effort will come from adding rapid random restarts to your solver. DPLL is known to exhibit heavy-tailed behavior, producing both short and long search times for instances depending on initial search conditions. Random restarts allow the solver to bail out of exponentially long searches of unfruitful assignments and give the solver more chances to find one of those short searches sooner.

Implementing two-watched-literals will produce the next big improvement because it eliminates a major backtracking cost. Backtracking is done exponentially often in the worst case, so any improvements there offer unequivocal improvements in search speed. Implementing two-watched-literals will require a significant overhaul of your solver, but it will teach you a lot about how real-world SAT solvers work.

Context

StackExchange Computer Science Q#63954, answer score: 2

Revisions (0)

No revisions yet.