Hacker News Reader

Does someone, with some experience on this subject, has an opinion on the best solver with binding in Python for a begginer? The OP use Z3 but also mentionned MiniZinc and I heard about Google OR-Tools.

View on HN

If you want to work in Python, I would either use OR-Tools which has a Python library or CPMpy which is a solver agnostic Python library using numpy style for modeling combinatorial optimization problems.

There is a Python package for MiniZinc, but it is aimed at structuring calls to MiniZinc, not as a modeling layer for MiniZinc.

Personally, I think it is better to start with constraint programming style modeling as it is more flexible, and then move to SMT style models like Z3 if or when it is needed. One of the reasons I think CP is a better initial choice is the focus on higher-level concepts and global constraints.

If you do want to start with SMT though, z3 has quite good bindings. I found it intuitive to use, and its ability to give you answers to very hard problems is like owning a magic wand.

It really depends on the kind of solving you want to do. Mathematical optimization, as in finding the cheapest/smallest/whatever solution that fits a problem? OR-Tools. Satisfaction problems, like finding counterexamples in rulesets or reverse engineering code? Z3.

Reply on news.ycombinator.com