No project description provided
The Cute SAT Constraint encoder Library for Python 3
PyCSCL is a collection of propositional logic constraint encoders. You can use it e.g. to reduce instances of NP-complete problems to instances of the Boolean satisifability (SAT) problem, benefitting from the availability of powerful off-the-shelf SAT solvers.
Though PyCSCL is designed not to depend on a specific SAT solver interface, it contains a simple and easy-to-use binding for SAT solvers implementing the IPASIR interface.
The versioning scheme of PyCSCL is Semantic Versioning 2.0.0.
PyCSCL has no dependencies beyond Python 3.7.
PyCSCL releases are distributed on the Python Package Index.
To be consistent with package naming conventions, the PyCSCL package is named
To install the latest PyCSCL release package, you can simply use
python3 -m pip install pycscl
Alternatively, you can check out this repository and install PyCSCL by creating a package yourself. Navigate to the PyCSCL directory and issue the command
python3 setup.py sdist
This will create a package
pycscl-<Version>.tar.gz file in the
dist. Now, you can install your custom PyCSCL package
python3 -m pip install <PathToPyCSCL>/dist/pycscl-<Version>.tar.gz
Cardinality (at-most-k) constraint encoders
- Binomial encoding
- LTSeq encoding
- Commander encoding
Gate constraint encoders
- AND, OR, binary XOR gates
- Binary MUX gates
- Half adder and full adder gates
Bitvector constraint encoders
- Bitvector AND, OR, XOR gates
- Ripple-carry bitvector adder and (2's complement) subtractor gates
- Parallel bitvector multiplier gate
- Unsigned bitvector divider and modulo gate
- Signed (2's complement) and unsigned bitvector comparison gates