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 … »
Modern SAT solvers: fast, neat and underused (part 3 of N)
In the previous two parts we used a SAT solver as a black box that we feed input into, and it will (usually quickly) spit out an answer. In this part, we will look at how SAT solvers work and what heuristics and other tricks they employ in their quest for performance. … »
Modern SAT solvers: fast, neat and underused (part 2 of N)
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. … »
Modern SAT solvers: fast, neat and underused (part 1 of N)
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. … »