Skip to main content

A Python library for prototyping with SAT oracles

Project description

A Python library providing a simple interface to a number of state-of-art Boolean satisfiability (SAT) solvers and a few types of cardinality encodings. The purpose of PySAT is to enable researchers working on SAT and its applications and generalizations to easily prototype with SAT oracles in Python while exploiting incrementally the power of the original low-level implementations of modern SAT solvers.

With PySAT it should be easy for you to implement a MaxSAT solver, an MUS/MCS extractor/enumerator, or any tool solving an application problem with the (potentially multiple) use of a SAT oracle.

Currently, the following SAT solvers are supported:

Cardinality encodings supported are implemented in C++ and include:

  • pairwise [6]

  • bitwise [6]

  • sequential counters [7]

  • sorting networks [3]

  • cardinality networks [1]

  • ladder [4]

  • totalizer [2]

  • modulo totalizer [5]

Usage

Boolean variables in PySAT are represented as natural identifiers, e.g. numbers from \(\mathbb{N}_{>0}\). A literal in PySAT is assumed to be an integer, e.g. -1 represents a literal \(\neg{x_1}\) while \(5\) represents a literal \(x_5\). A clause is a list of literals, e.g. [-3, -2] is a clause \((\neg{x_3} \vee \neg{x_2})\).

The following is a trivial example of PySAT usage:

>>> from pysat.solvers import Glucose3
>>>
>>> g = Glucose3()
>>> g.add_clause([-1, 2])
>>> g.add_clause([-2, 3])
>>> print g.solve()
>>> print g.get_model()
...
True
[-1, -2, -3]

Another example shows how to extract unsatisfiable cores from a SAT solver given an unsatisfiable set of clauses:

>>> from pysat.solvers import Minisat22
>>>
>>> with Minisat22(bootstrap_with=[[-1, 2], [-2, 3]]) as m:
...     print m.solve(assumptions=[1, -3])
...     print m.get_core()
...
False
[-3, 1]

Finally, the following example gives an idea of how one can extract a proof (supported by Glucose3 and Lingeling only):

>>> from pysat.formula import CNF
>>> from pysat.solvers import Lingeling
>>>
>>> formula = CNF()
>>> formula.append([-1, 2])
>>> formula.append([1, -2])
>>> formula.append([-1, -2])
>>> formula.append([1, 2])
>>>
>>> with Lingeling(bootstrap_with=formula.clauses, with_proof=True) as l:
...     if l.solve() == False:
...         print(l.get_proof())
...
['2 0', '1 0', '0']

PySAT usage is detailed in the provided examples. For instance, one can see there simple PySAT-based implementations of

  • Fu&Malik algorithm for MaxSAT [8]

  • CLD-like algorithm for MCS extraction and enumeration [10]

  • LBX-like algorithm for MCS extraction and enumeration [11]

  • Deletion-based MUS extraction [9]

Installation

The simplest way to get and start using PySAT is to install the latest stable release of PySAT from PyPI:

pip install python-sat

Alternatively, you can clone this repository and do the following with your local copy:

python setup.py install

or (if you choose a directory to install PySAT into)

python setup.py install --prefix=<where-to-install>

Both options (i.e. via pip or setup.py) are supposed to download and compile all the supported SAT solvers as well as prepare the installation of PySAT.

License

This project is licensed under the MIT License - see the LICENSE file for details.

Project details


Release history Release notifications | RSS feed

Download files

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

Source Distribution

python-sat-0.1.2dev0.tar.gz (68.3 kB view hashes)

Uploaded Source

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page