1
$\begingroup$

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.

$\endgroup$
  • 3
    $\begingroup$ I don't understand your question. You say that all you need to do is implement some improvement and it doesn't really matter how good it is. You have several possible improvements so just implement one or more of them. Mission accomplished, no? $\endgroup$ – David Richerby Sep 27 '16 at 13:20
  • 1
    $\begingroup$ This is an open-ended, list-style question; we don't like that. Can you specify more closely what you want to that only a few answers are a good fit? $\endgroup$ – Raphael Sep 27 '16 at 18:49
  • $\begingroup$ @DavidRicherby I'm sorry if my question is not very clear. I do need to implement enough improvements to pass some benchmark that the college has, and from there the better it performs, the better the grade. I don't want to make something extremely good, but I would be happy if it performed a bit better than what they ask me for =) I don't want to spend too much time, however, so I figured I would ask here what's the best basic optimizations I can implement without it being an overkill. $\endgroup$ – user1843790 Sep 28 '16 at 13:33
  • $\begingroup$ @Raphael I apologize. I just wanted to hear about basic DPLL optimizations and how much of a performance improvement they were, so I'm not sure how to reword that. Feel free to edit the question if you come up with a better way. $\endgroup$ – user1843790 Sep 28 '16 at 13:38
2
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ I've spent time programming solvers, and totally agree with random restarts. They are easy to implement, and will improve performance. (Well, I also agree with watched literals, but random restarts are easier to implement). $\endgroup$ – Juho Sep 27 '16 at 16:08
  • $\begingroup$ Do you think basic DPLL with 2WL and random restarts (but without CDCL) is good enough to crack 1500 clauses with 300 variables? $\endgroup$ – Martin Berger Sep 27 '16 at 16:11
  • $\begingroup$ @MartinBerger Where are these numbers coming from? We know that it's not the size of the instance that matters, but the structure of it. I can give much smaller instances that will not be cracked easily even with state-of-the-art solvers. $\endgroup$ – Juho Sep 27 '16 at 16:14
  • $\begingroup$ @MartinBerger Ah, the numbers come from the question :-) But still, the answer depends entirely on the structure of the instance. $\endgroup$ – Juho Sep 27 '16 at 16:18
  • $\begingroup$ Variable and clause counts are only a very loose indication of the hardness of a SAT instance. See Backbones and Backdoors in Satisfiability for instance. For random k-SAT instances, a clause/variable ratio in the phase transition region generally indicates a hard instance. For structured problems, the counts may offer no indication at all. $\endgroup$ – Kyle Jones Sep 27 '16 at 16:22
0
$\begingroup$

I suggest to implement CDCL with 1-UIP (UIP = unique implication point) as heuristic to minimise the learned clause. Use 2WL to speed up unit-propagation. See here for a basic implementation of CDCL in Python.

Things like VSIDS make sense only for CDCL, and are used to prune learned clauses. CDCL has a tendency to learn too much. But if you have only approx. 1.5k clauses, you should probably be able to live without pruning,

$\endgroup$
  • $\begingroup$ Thank you very much for the answer, Martin. I forgot to add that the clauses are pretty small. How good is 2WL for that case? $\endgroup$ – user1843790 Sep 27 '16 at 12:41
  • $\begingroup$ CDCL may generate large learned clauses. Try it out with another unit propagation algorithm first. If you abstract your unit-prop well, you should be able to replace the unit-prop without touching the rest of the code. Note however that the 2WL affects how you know that DPLL has terminated. $\endgroup$ – Martin Berger Sep 27 '16 at 13:12
  • $\begingroup$ Can you give evidence that shows that these proposals are "best" in some sense? $\endgroup$ – Raphael Sep 27 '16 at 18:50
  • $\begingroup$ @Raphael No. That's a hunch of mine, based on my own experiments with SAT solving. I don't think it's well understood which SAT-solving heuristics work well and why. $\endgroup$ – Martin Berger Sep 27 '16 at 20:40

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.