Is there a wbo-like SAT-Solver for Python?

Question

Is there a Python-Module / Program, that solves a SAT Problem? Probably a weighted Boolean one. (To be specific, something like wbo)

Or if not are there maybe bindings, or an API to use one of those solvers.

I don't think i could programm one myself in the time i have right now.

Answer 1

In order to solve SAT problems I would suggest using MiniSat (http://minisat.se), Glucose (https://www.lri.fr/~simon/?page=glucose) or Picosat (http://fmv.jku.at/picosat) and there are others. In the case of pseudo-boolean optimization I know of MiniSat+ (http://minisat.se/MiniSat+.html) and Gurobi (http://www.gurobi.com). I think all of them are free, except Gurobi, which offers trial and academic licences).

All of them offer a command line interface with input and output files that are easily generated/read from within Python. Moreover, Gurobi features a full Python shell.