Install & Compatibility
Where this runs
tested against v1.9.dev5 · pip install
no network on importno background threads
Install × environment matrix
Each cell = how many times install + import succeeded across repeated harness runs. Partial = flaky.
glibc = Debian/Ubuntu slim · musl = Alpine Linux
51MB installed
● package 51MB
Code
Verified usage
Verified import paths — ran on the pinned version, not inferred.
Solver
✓ from pysat.solvers import Solver
Glucose3
✓ from pysat.solvers import Glucose3
✗ from python_sat.solvers import Glucose3
The PyPI package name is 'python-sat', but the Python import module is 'pysat'.
CNF
✓ from pysat.formula import CNF
✗ import python_sat
Core functionalities are within submodules like 'formula' and 'solvers', not directly under the top-level 'pysat' module.
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())
Debug
Known issues
gotchaThe 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.fixEnsure your `pip install` command is `pip install python-sat` and your Python code uses `import pysat`.
affects: All versions
breakingInstallation 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++`.fixBefore 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.
affects: All versions
gotchaPySAT 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.fixPeriodically update the library using `pip install -U python-sat` and review release notes for significant changes.
affects: All versions
gotchaSome 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.fixConsult 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.
affects: All versions (specific to non-incremental solvers like Kissat)
Errors
Common errors & fixes
error: Microsoft Visual C++ 14.0 or greater is required.
PySAT relies on compiling C/C++ extensions, and the required build tools for Windows (part of Visual Studio) are missing or not correctly configured.
fixInstall 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'
Incorrect import statement. The PyPI package `python-sat` should be imported as `pysat`.
fixChange 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.
Attempting to add clauses to a non-incremental solver (like Kissat) after it has already been used to solve a formula.
fixFor 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'
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).
fixEnsure 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.
Upgrade
Version history
1.9.dev5latest on PyPI · released Jun 10, 2026
Audit
Dependencies
sixrequiredCompatibility layer, required for installation process.
aigeroptionalProvides AIGER format support for SAT instances.
approxmcoptionalIntegrates ApproxMCv4 tool for approximate model counting.
cryptosatoptionalProvides an interface to CryptoMiniSat5 for cryptographic problems.
pbliboptionalProvides basic functionality for pseudo-Boolean constraints.