PySAT: A Python Library for SAT Oracles

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.