{"id":9261,"library":"python-sat","title":"PySAT: A Python Library for SAT Oracles","description":"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.","status":"active","version":"1.9.dev2","language":"en","source_language":"en","source_url":"https://github.com/pysathq/pysat","tags":["SAT solver","satisfiability","Boolean logic","MaxSAT","MUS","MCS","constraint programming"],"install":[{"cmd":"pip install python-sat","lang":"bash","label":"Basic Installation"},{"cmd":"pip install 'python-sat[aiger,approxmc,cryptosat,pblib]'","lang":"bash","label":"With Optional Dependencies"}],"dependencies":[{"reason":"Compatibility layer, required for installation process.","package":"six","optional":false},{"reason":"Provides AIGER format support for SAT instances.","package":"aiger","optional":true},{"reason":"Integrates ApproxMCv4 tool for approximate model counting.","package":"approxmc","optional":true},{"reason":"Provides an interface to CryptoMiniSat5 for cryptographic problems.","package":"cryptosat","optional":true},{"reason":"Provides basic functionality for pseudo-Boolean constraints.","package":"pblib","optional":true}],"imports":[{"symbol":"Solver","correct":"from pysat.solvers import Solver"},{"note":"The PyPI package name is 'python-sat', but the Python import module is 'pysat'.","wrong":"from python_sat.solvers import Glucose3","symbol":"Glucose3","correct":"from pysat.solvers import Glucose3"},{"note":"Core functionalities are within submodules like 'formula' and 'solvers', not directly under the top-level 'pysat' module.","wrong":"import python_sat","symbol":"CNF","correct":"from pysat.formula import CNF"}],"quickstart":{"code":"from pysat.solvers import Solver\nfrom pysat.formula import CNF\n\n# Create a CNF formula for (x1 or not x2) and (not x1 or x2)\ncnf = CNF()\ncnf.append([1, -2])\ncnf.append([-1, 2])\n\n# Initialize a Glucose3 solver\nwith Solver(name='glucose3') as solver:\n    solver.append_formula(cnf)\n    \n    if solver.solve():\n        model = solver.get_model()\n        print(f\"Satisfiable. Model: {model}\")\n    else:\n        print(\"Unsatisfiable.\")\n\n# Example with specific solver import\nfrom pysat.solvers import Minisat22\nwith Minisat22(bootstrap_with=[[-1, 2], [-2, 3]]) as m:\n    print(m.solve(assumptions=[1, -3]))\n    print(m.get_core())\n","lang":"python","description":"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."},"warnings":[{"fix":"Ensure your `pip install` command is `pip install python-sat` and your Python code uses `import pysat`.","message":"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.","severity":"gotcha","affected_versions":"All versions"},{"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.","message":"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++`.","severity":"breaking","affected_versions":"All versions"},{"fix":"Periodically update the library using `pip install -U python-sat` and review release notes for significant changes.","message":"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.","severity":"gotcha","affected_versions":"All versions"},{"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.","message":"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.","severity":"gotcha","affected_versions":"All versions (specific to non-incremental solvers like Kissat)"}],"env_vars":null,"last_verified":"2026-04-16T00:00:00.000Z","next_check":"2026-07-15T00:00:00.000Z","problems":[{"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.","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.","error":"error: Microsoft Visual C++ 14.0 or greater is required."},{"fix":"Change your import statement from `from python_sat.solvers import Solver` to `from pysat.solvers import Solver` (or similarly for other modules).","cause":"Incorrect import statement. The PyPI package `python-sat` should be imported as `pysat`.","error":"ModuleNotFoundError: No module named 'pysat.solvers'"},{"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).","cause":"Attempting to add clauses to a non-incremental solver (like Kissat) after it has already been used to solve a formula.","error":"TypeError: Cannot add clauses for non-incremental solver."},{"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.","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).","error":"AttributeError: 'Solver' object has no attribute 'get_core'"}]}