An interface to SAT solver tools (like minisat)
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.
examples Ran Python-Modernize Aug 17, 2018
.gitignore Ignore dist directory Aug 17, 2018
.travis.yml [CI] modify list of supported python versions Aug 17, 2018
LICENSE OSI Approved BSD License Sep 25, 2014 Add ability to create Cnf object from string of Boolean formula Aug 17, 2018
requirements.txt CI Aug 17, 2018 Fix version numbers Aug 17, 2018

Build Status


Satispy is a Python library that aims to be an interface to various SAT (boolean satisfiability) solver applications.

Supported solvers:

Support for other solvers should be fairly easy as long as they accept the DIMACS CNF SAT format.


You can grab the current version from pypi:

$ sudo pip install satispy

Or you can download a copy from, and runs

$ sudo ./ install

in the directory of the project.

If you want to develop on the library, use:

$ ./ develop

You can run the tests found in the test folder by running

How it works

You need a SAT solver to be installed on your machine for this to work.

Let's see an example:

from satispy import Variable, Cnf
from satispy.solver import Minisat

v1 = Variable('v1')
v2 = Variable('v2')
v3 = Variable('v3')

exp = v1 & v2 | v3

solver = Minisat()

solution = solver.solve(exp)

if solution.success:
    print "Found a solution:"
    print v1, solution[v1]
    print v2, solution[v2]
    print v3, solution[v3]
    print "The expression cannot be satisfied"

This program tries to satisfy the boolean expression

v1 & v2 | v3

You can make this true by assigning true to all variables for example, but there are other solutions too. This program finds a single arbitrary solution.

First, the program imports the various classes so we can build an expression and try to solve it.

Every expression is in CNF form, but we don't have to enter the expression in it. The Cnf class takes care of the proper arranging of the boolean terms.

Expressions can be built by creating variables and gluing them together arbitrarily with boolean operators:

  • NOT: - (unary)
  • AND: &
  • OR: |
  • XOR: ^

The solver class Minisat is used to solve the formula.

Note: the Minisat class creates two temporary files, so it needs write access to the system's temporary directory

The returned solution can be checked by reading the "success" boolean flag.

Then, the solution can be queried for variable assignments by using it like a dictionary. Note that Variable objects are used, not strings.

(This very example can be found in the examples directory)

Parsing Boolean expressions

It is also possible to create a Cnf object directly, without first creating Variable objects:

from satispy import CnfFromString
from satispy.solver import Minisat

exp, symbols = CnfFromString.create("v1 & v2 | v3")

solver = Minisat()

solution = solver.solve(exp)

if solution.success:
    print "Found a solution:"
    for symbol_name in symbols.keys():
        print "%s is %s" % (symbol_name, solution[symbols[symbol_name]])
    print "The expression cannot be satisfied"