I was lucky enough to attend a Dagstuhl seminar titled “Bringing CP, SAT & SMT Together” earlier this week, and learned about some really cool work I hadn’t previously heard of, especially in the realm of constraint satisfaction and optimization. There were plenty of other of great talks and discussions, but below are the projects I made a note to play around with.
MiniZinc
“MiniZinc is a free and open-source constraint modeling language.
You can use MiniZinc to model constraint satisfaction and optimization problems in a high-level, solver-independent way, taking advantage of a large library of pre-defined constraints. Your model is then compiled into FlatZinc, a solver input language that is understood by a wide range of solvers.“
There are even a couple of Coursera courses on the topic.
https://www.minizinc.org/
https://www.coursera.org/learn/basic-modeling
https://www.coursera.org/learn/advanced-modeling
Unison
“Unison is a simple, flexible, and potentially optimal tool that performs integrated register allocation and instruction scheduling using constraint programming as a modern method for combinatorial optimization.“
https://unison-code.github.io/
Approximate Model Counting
Blog post by Mate Soos (author of cryptominisat), with code:
“Approximate model counting allows to count the number of solutions (or “models”) to propositional satisfiability problems. This problem seems trivial at first given a propositional solver that can find a single solution: find one solution, ban it, ask for another one, ban it, etc. until all solutions are counted. The issue is that sometimes, the number of solutions is 2^50 and so counting this way is too slow. There are about 2^266 atoms in the universe, so counting anywhere near that is impossible using this method.“
—
Sean Heelan's Blog 