Hacker News Reader

Comment by mathgenius | Hacker News Reader

Do any of these have python interfaces?

Z3 has a python interface. This said, SMT is an extension of SAT, and you're likely to use a SMT solver even for "just" SAT problems. Most SMT solvers support the SMT-LIB [1] file format, which is easy to generate from python. It also lets you switch engine easily.

Also, there are other kinds of interesting solvers. For constraint problems, one can check minizinc [2]. A bit like SMT-LIB, it's a language to describe constraint problems that is supported by many solvers. It's commonly used with gecode [3]. For many problems using minizinc will be much easier than trying to convert the problem in SAT (or even SMT) format.

Happy hacking, it's a fascinating domain!

[1] http://smtlib.cs.uiowa.edu/ [2] http://www.minizinc.org/ [3] http://www.gecode.org/

In pySMT, we have been working on making the simplicity of the z3 python interface available to other solvers both through SMT-LIB interfaces, but also native API integration for SMT/SAT solvers and OBDDs.

We are always glad to get more feedback!

https://github.com/pysmt/pysmt

In looking over whether the license would be amenable to distribution as part of a game, I noticed that your github page links to pysmt.org at the top, but that's only a redirect back to the github page :p

Eheh, we tried for some time to come up with a good webpage. At the end of the day, this is a library for developers, and as such we decided that the Github page is the most meaningful place to start. We put a lot of work in the main README, with revisions after each release, and we have a readthedocs for detailed documentation. Nevertheless, the github page gives you also other insights on what is the development status of the library (currently active but not daily), and areas of targeted improvement.

Re the licensing, pySMT is open-source and distributed under APACHE 2.0 .

Pysat does: https://pysathq.github.io/docs/html/index.html

Reply on news.ycombinator.com