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.

_images/OptiLog_Arch.png

The main architecture of OptiLog is composed of the four main modules of the end-user OptiLog API that supports the creation of SAT based systems and the iSAT interface for SAT solver developers.

The Formula module:

The Formula module provides classes for the manipulation of SAT, MaxSAT and QBF formulas.

The SAT Solver module:

The SAT Solver module provides bindings through the Python Interface PyiSAT to SAT solvers implementing the iSAT interface.

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.