miniblog.

← Back to all posts
Sep 24, 2020 at 04:58
A nifty "skill tree" approach to mapping out the requirements in Rust's trait solver: https://rust-lang.github.io/wg-traits/roadmap/skill-tree.html (From https://blog.rust-lang.org/inside-rust/2020/03/28/traits-sprint-1.html)
Redirect

Related Posts

Dec 10, 2022 at 22:45
Computing optimal 8501 instructions for rotations using an SMT solver and Racket with Rosette:
Synthesizing optimal 8051 code — whitequark's lab notebook
Feb 10, 2020 at 00:02
Applying an SMT solver to find missed optimisation opportunities in LLVM's arithmetic tooling: https://blog.regehr.org/archives/1714
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.