miniblog.

← Back to all posts
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)
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.

Related Posts

Jun 22, 2019 at 22:35
The US Navy is exploring ships that are more highly automated. The crew is smaller, and their roles are generalist problem solvers.
At Work, Expertise Is Falling Out of Favor
At Work, Expertise Is Falling Out of Favor
These days, it seems, just about all organizations are asking their employees to do more with less. Is that actually a good idea?
Aug 5, 2018 at 01:04
SAT solvers are underused in tech: an introduction and a fun example of sudoku solving: https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/
Aug 22, 2017 at 22:37
AST canonicalisation in arithmetic solvers: https://blog.plover.com/math/24-puzzle-2.html (interesting, I've only seen canonicalisation in compilers previously)
Recognizing when two arithmetic expressions are essentially the same
Recognizing when two arithmetic expressions are essentially the same
From the highly eclectic blog of Mark Dominus