{"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.","language":"python","status":"active","last_verified":"Thu Apr 16","install":{"commands":["pip install python-sat","pip install 'python-sat[aiger,approxmc,cryptosat,pblib]'"],"cli":null},"imports":["from pysat.solvers import Solver","from pysat.solvers import Glucose3","from pysat.formula import CNF"],"auth":{"required":false,"env_vars":[]},"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.","tag":null,"tag_description":null,"last_tested":null,"results":[]},"compatibility":null}