11

Modern SAT solvers: fast, neat and underused (part 1.5 of N)

 4 years ago
source link: https://codingnest.com/modern-sat-solvers-fast-neat-and-underused-part-1-5-of-n/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
neoserver,ios ssh client

Modern SAT solvers: fast, neat and underused (part 1.5 of N)

In part 1 of this series, we built a Sudoku solver based on translating Sudoku to SAT and then giving the resulting SAT instance to a SAT solver. We also benchmarked our solver and found out that it, unsurprisingly, loses to the state of the art of Sudoku solvers. Since then, I convinced[1] a couple of my friends to also write a C++ sudoku solver, and we can compare our solver against those.

We have 2 other solvers to compare our solver to, one written by Aleš Hrabalík, and one written by Ben Steffan (BiCapitalize on Twitter/Discord).

Implementations

Aleš's implementation can be found in his GitHub repo, and the algorithm itself is a simple backtracking solver. It has been savagely optimized though and relies heavily on CPU's native handling of lsb and popcnt instructions. According to Aleš, it took roughly 8 hours to write, but he has had previous experience with writing a Sudoku solver in C++.

Ben's implementation can also be found in his GitHub repo, and it is an implementation of Knuth's Algorithm X using Dancing Links. According to Ben, it took him roughly 20 hours to write, but he had no previous experience with writing a Sudoku solver.

Benchmark results

The benchmarked versions were commits 132c1d4f for Aleš's solver, 243f546d for Ben's solver and 4894ff6f for our SAT-based solver. The inputs used for benchmarking was the same set of 95 hard Sudokus as in part 1, on the same machine using the same compiler and environment.

These are the results:

3-plot

As we can see, Aleš's solver has the fastest single solution time, and also the fastest average solution time. However, it also has the longest tail, taking roughly 40ms for the slowest of the inputs. The other two solvers have significantly less runtime variance, and at this level of detail, are basically identical as far as their average runtime goes.

Let's zoom in a bit.

2-plot

Now we can see that the SAT-based solver performs slightly better, but the differences in both best and average performance are small enough as to be pointless. The most interesting part of comparing these two is that the SAT-based solver is comparatively more consistent and has a shorter tail.

Conclusion

We got 3 different Sudoku solvers written in "reasonable prototyping time", that is a day or two. We found out that the performance of our SAT-based solver is competitive with the other 2 dedicated Sudoku solver. We also found out that it took other people more time to write a direct Sudoku solver[2] than it took us to write a solver based on translating SAT to sudoku.

That is all for part 1.5.

Part 2 shows how to implement a SAT-based solver for master-key systems.

  1. Read as "pestered until they did it". ↩︎

  2. In the case of Ben's solver, it took significantly more time to implement it than it took to implement the SAT-based solver. ↩︎


report

Recommend

About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK