I found myself once again writing a long forum post about the problems with standard-provided random number generation facilities (both C++'s <random>, and C's rand) in C++. Since I keep writing these, I decided to write it all down into one blog post so that I can link it to people later.
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
I just got home from the second conference I gave a talk at during September and decided to write about my experiences while I am slowly decompressing.
The previous post in this series was a quick introduction to the world of SAT and SAT solvers. In this post, we will convert a harder real-world problem, namely _master-key system_, into SAT and explore some of the more advanced techniques used to efficiently convert problems to SAT.
Before I started doing research, I saw SAT solvers as academically interesting but without practical uses ouside of other academic applications. I've since then changed my mind, and I want to change yours, because modern SAT solvers are neat, fast and almost criminally underused by the industry.