Skip to main content

An interface to SAT solver tools (like minisat)

Project description

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

As of this version, only minisat is supported (and it’s pretty cool, so we should be fine with it for a wile ;) )

Installing

You can grab the current version from pypi:

$ sudo pip install satispy

Or you can download a copy from https://github.com/netom/satispy, and runs

$ sudo ./setup.py install

in the directory of the project.

You can run the tests found in the test folder by running run_tests.py.

How it works

You need minisat 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]
else:
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: ^
  • IMPLICATION >>

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)

Project details


Release history Release notifications

History Node

1.0

History Node

1.0a5

This version
History Node

1.0a4

History Node

1.0a3

History Node

1.0a2

History Node

1.0a1

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Filename, size & hash SHA256 hash help File type Python version Upload date
satispy-1.0a4.tar.gz (9.4 kB) Copy SHA256 hash SHA256 Source None Jun 4, 2013

Supported by

Elastic Elastic Search Pingdom Pingdom Monitoring Google Google BigQuery Sentry Sentry Error logging CloudAMQP CloudAMQP RabbitMQ AWS AWS Cloud computing Fastly Fastly CDN DigiCert DigiCert EV certificate StatusPage StatusPage Status page