OptiLog: A Framework for SAT-based Systems¶
We present OptiLog, a new Python framework for rapid prototyping of SAT-based systems. OptiLog allows to use and integrate SAT solvers currently developed in C/C++ just by implementing the iSAT C++ interface. It also provides a Python binding to the PBLib C++ toolkit for encoding Pseudo Boolean and Cardinality constraints. Finally, it leverages the power of automatic configurators by allowing to easily create configuration scenarios including multiple solvers and encoders.
- The Formula module:
The Formula module provides classes for the manipulation of SAT, MaxSAT and QBF formulas.
- The SAT Solver module:
- The PB Encoder module:
The PB Encoder module provides access to encoders Pseudo-Boolean and Cardinality into SAT.
- The Automatic Configuration module:
The Automatic Configuration module provides support to automatically configure Python functions.