{"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":"python","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,"search_vec":"'1.9':79 'art':29 'boolean':30,72,94 'c/c':54 'cardin':68 'constraint':73,99 'current':76 'dev2':80 'develop':38 'easili':40 'enabl':35 'encod':65 'exploit':47 'follow':82 'frequent':88 'implement':55 'increment':19 'interfac':20 'level':53 'librari':4,12,61 'linear':67 'logic':95 'low':52 'low-level':51 'maxsat':96 'mcs':98 'model':86 'modern':57 'mus':97 'offer':62 'oracl':7,44 'power':49 'program':100 'proposit':64 'prototyp':41 'provid':14 'pseudo':71 'pseudo-boolean':70 'pysat':1,8 'python':3,11,46 'releas':85 'research':36 'roll':84 'sat':6,32,43,58,91 'satisfi':31,93 'simpl':16 'small':89 'solver':33,59,92 'state':26 'state-of-the-art':25 'unifi':18 'updat':90 'varieti':23 'various':63 'version':78","created_at":"2026-04-16T18:49:18.184179+00:00","updated_at":"2026-04-16T18:49:18.184179+00:00","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'"}],"ecosystem":"pypi","meta_description":null,"install_score":null,"quickstart_score":null,"quickstart_tag":null,"pypi_latest":"1.9.dev5","cli_name":"","cli_version":null,"type":"library","homepage":"https://pysathq.github.io","github":"https://github.com/pysathq/pysat","docs":null,"changelog":null,"pypi":"https://pypi.org/project/python-sat/","npm":null,"openapi_spec":null,"status_page":null,"smithery":null,"categories":["ai-ml"],"base_url":null,"auth_type":null,"provenance":{"verified_status":"passing","verified_at":"2026-06-28","last_verified":"2026-06-28","next_check":"2026-07-28","install_tag":null}}