PySAT: A Python Library for SAT Oracles

1.9.dev2 · active · verified Thu Apr 16

PySAT is a Python library that provides a simple and unified incremental interface to a variety of state-of-the-art Boolean satisfiability (SAT) solvers. It enables researchers and developers to easily prototype with SAT oracles in Python, exploiting the power of low-level C/C++ implementations of modern SAT solvers. The library offers various propositional encodings for linear (cardinality and pseudo-Boolean) constraints. It is currently at version 1.9.dev2 and follows a rolling release model with frequent, small updates.

Common errors

```
error: Microsoft Visual C++ 14.0 or greater is required.
```
cause PySAT relies on compiling C/C++ extensions, and the required build tools for Windows (part of Visual Studio) are missing or not correctly configured.

fix Install the 'Build Tools for Visual Studio' (e.g., Visual Studio 2019 or newer) from Microsoft, ensuring the 'Desktop development with C++' workload is selected. Alternatively, try installing in a Linux environment or WSL.
```
ModuleNotFoundError: No module named 'pysat.solvers'
```
cause Incorrect import statement. The PyPI package `python-sat` should be imported as `pysat`.

fix Change your import statement from `from python_sat.solvers import Solver` to `from pysat.solvers import Solver` (or similarly for other modules).
```
TypeError: Cannot add clauses for non-incremental solver.
```
cause Attempting to add clauses to a non-incremental solver (like Kissat) after it has already been used to solve a formula.

fix For non-incremental solvers, all clauses must be added during initialization or before the first call to `solve()`. For incremental problem-solving, use a solver that explicitly supports incrementality (e.g., Glucose, CaDiCaL).
```
AttributeError: 'Solver' object has no attribute 'get_core'
```
cause The specific solver instance used does not support UNSAT core extraction (e.g., Kissat does not support assumption-based solving, which is required for core extraction).

fix Ensure you are using a SAT solver that supports UNSAT core extraction, such as Minisat22, Glucose3, or Lingeling, and that it was invoked with assumptions or in a context where a core can be derived.

Warnings

gotcha The PyPI package is named `python-sat`, but the library is imported as `pysat`. There is an unrelated library also called `pysat` (Python Satellite Data Analysis Toolkit), leading to common confusion. Always use `import pysat` for this library.
Fix: Ensure your `pip install` command is `pip install python-sat` and your Python code uses `import pysat`.
breaking Installation requires system-level dependencies: a C/C++11 compiler (e.g., GCC or Clang), Python headers, and zlib headers. On macOS, Clang is preferred over GCC to avoid compilation issues related to `--stdlib=libc++`.
Fix: Before installing, ensure you have a C++11 compliant compiler and necessary development headers. For macOS, set `export CC=/usr/bin/clang` before installation if encountering issues.
gotcha PySAT uses a 'rolling release' model, meaning frequent small updates rather than major version bumps. This necessitates regular `pip install -U python-sat` to stay up-to-date and benefit from bug fixes and new features, but can also introduce subtle changes.
Fix: Periodically update the library using `pip install -U python-sat` and review release notes for significant changes.
gotcha Some integrated SAT solvers (e.g., Kissat) are non-incremental. Using functions like `add_clause()` after calling `solve()` with these solvers can lead to undefined behavior. They also do not support model enumeration or UNSAT core extraction.
Fix: Consult the `pysat.solvers` documentation to understand the capabilities and limitations of each solver. For incremental solving, model enumeration, or core extraction, use compatible solvers like CaDiCaL or Glucose.

Install

pip install python-sat Basic Installation
pip install 'python-sat[aiger,approxmc,cryptosat,pblib]' With Optional Dependencies

Imports

Solver
```
from pysat.solvers import Solver
```
Glucose3
wrong:
```
from python_sat.solvers import Glucose3
```
correct:
```
from pysat.solvers import Glucose3
```
The PyPI package name is 'python-sat', but the Python import module is 'pysat'.
CNF
wrong:
```
import python_sat
```
correct:
```
from pysat.formula import CNF
```
Core functionalities are within submodules like 'formula' and 'solvers', not directly under the top-level 'pysat' module.

Quickstart

This quickstart demonstrates how to create a Conjunctive Normal Form (CNF) formula and solve it using different SAT solvers available through the PySAT interface. It also shows how to get a model or an unsatisfiable core if applicable.

from pysat.solvers import Solver
from pysat.formula import CNF

# Create a CNF formula for (x1 or not x2) and (not x1 or x2)
cnf = CNF()
cnf.append([1, -2])
cnf.append([-1, 2])

# Initialize a Glucose3 solver
with Solver(name='glucose3') as solver:
    solver.append_formula(cnf)
    
    if solver.solve():
        model = solver.get_model()
        print(f"Satisfiable. Model: {model}")
    else:
        print("Unsatisfiable.")

# Example with specific solver import
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())

view raw JSON →