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 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.


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.

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.


Slightly chilled attendees




Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.