OptiLog: A Framework for SAT-based Systems
OptiLog is a Python framework for rapid prototyping of SAT-based systems. OptiLog includes functionality for loading and creating formulas, state of the art SAT solvers, high level formula modelling, pseudo boolean and cardinality encodings, automatic configuration and experiment running and parsing.
OptiLog is designed to be simple and efficient. OptiLog can be used by field experts for tasks such as algorithm design, research and benchmarking, but it has also been successfully deployed in undergraduate Computational Logic courses. Moreover, OptiLog has been designed from the ground up to be modular and extensible through the abstract iSAT C++ interface.
Why OptiLog
OptiLog has a fully modular dynamic Python binding generator for SAT solvers. This means that integrating new SAT solvers into OptiLog is as simple as implementing a C++ interface, and doesn’t require any Python C API knowledge!
On top of that, OptiLog provides all the functionality required to develop and deploy complete SAT-based systems. We provide access to state of the art automatic configuration tools to configure any kind of algorithm (not limited to SAT) as well as experiment-running and log-parsing modules.
Architecture
The main architecture of OptiLog is composed by the seven main modules of the end-user OptiLog API that support the creation of SAT based systems and the iSAT interface for SAT solver developers.
- The Modelling module:
The Modelling module provides a rich and compact formalism to model problems. In particular, this module allows modelling problems with non-CNF Boolean and Pseudo Boolean expressions that can be automatically transformed into the SAT formula provided by the Formulas module.
- The Formulas module:
The Formulas module provides tools to load and manipulate SAT, MaxSAT, and QBF formulas.
- The Encoders module:
The Encoders module provides access to a set of encoders that can be used to translate constraints from one language to another. This module is currently composed of encoders for Pseudo-Boolean and Cardinality constraints into SAT.
- The Solvers module:
The Solvers module provides dynamic Python bindings for Python. It currently supports Solvers through the PyiSAT. These SAT solvers implement the iSAT interface.
- The Tuning module:
The Tuning module provides support to automatically configure Python functions.
- The Running module:
The Running module provides support to automatically generate execution scenarios that run experiments and collect logs.
- The Blackbox module:
The Blackbox module allows to encapsulate external applications into Python objects, which enables its interaction with the other modules from Optilog such as the Running module or the Tuning module.
Citing OptiLog
If you use OptiLog in your research, please cite our work:
@InProceedings{alos_et_al:LIPIcs.SAT.2022.25,
author = {Al\`{o}s, Josep and Ans\'{o}tegui, Carlos and Salvia, Josep M. and Torres, Eduard},
title = {{OptiLog V2: Model, Solve, Tune and Run}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {25:1--25:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16699},
URN = {urn:nbn:de:0030-drops-166996},
doi = {10.4230/LIPIcs.SAT.2022.25},
annote = {Keywords: Tool framework, Satisfiability, Modelling, Solving}
}