Some Cool Projects from a Dagstuhl Seminar on SAT, SMT and CP

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.

https://www.msoos.org/2018/12/how-approximate-model-counting-works/

 

Slightly chilled attendees