No project description provided
Project description
PyCSCL 0.1.0
PyCSCL is a collection of boolean 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.
Documentation
Encoders
Cardinality (at-most-k) constraint encoders
- Binomial encoding
- LTSeq encoding
Package: cscl.cardinality_constraint_encoders
Gate constraint encoders
- AND, OR, binary XOR gates
- Binary MUX gates
- Half adder and full adder gates
Package: cscl.basic_gate_encoders
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
Package: cscl.bitvector_gate_encoders
Examples
examples.factorization
: integer factorization problem encoderexamples.sudoku
: SAT-based Sudoku solverexamples.smt_qfbv_solver
(under construction): simple QF_BV SMT solver
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
pycscl-0.1.0.tar.gz
(51.6 kB
view hashes)