miniblog.

Wilfred Hughes

Aug 22, 2018 at 18:41

Elegant demo of SAT solvers: take a list of locks and which keys should unlock the (e.g. master keys unlock multiple), plus a set of manufacturing constraints. Feed it to a solver and calculate how to cut all the keys! https://codingnest.com/modern-sat-solvers-fast-neat-and-underused-part-2-of-n/ A real industry usecase of SAT.

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.