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 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.