OptiLog: A Framework for SAT-based Systems
===============================================

.. image:: optilog/images/OptiLog_Arch.png
    :align: center

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 :ref:`end-user OptiLog API <enduser_index>` that support the creation of SAT based systems and the :ref:`iSAT <isat-interface>` interface for :ref:`SAT solver developers <solverdevel_index>`.

The :ref:`Modelling <modelling-module>` 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 :ref:`Formulas <formula-module>` module:
    The *Formulas* module provides tools to load and manipulate SAT, MaxSAT, and QBF formulas.

The :ref:`Encoders <encoders-module>` 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 :ref:`Pseudo-Boolean and Cardinality <encoders-module>` constraints into SAT.

The :ref:`Solvers <solvers-module>` module:
    The *Solvers* module provides dynamic Python bindings for Python.
    It currently supports :ref:`Solvers <solvers-module>` through the :ref:`PyiSAT <pyisat>`. These SAT solvers implement the :ref:`iSAT <isat-interface>` interface.

The :ref:`Tuning <tuning-module>` module:
    The *Tuning* module provides support to automatically configure
    Python functions.

The :ref:`Running <running-module>` module:
    The *Running* module provides support to automatically generate execution scenarios
    that run experiments and collect logs.

The :ref:`Blackbox <blackbox-module>` 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}
    }

.. toctree::
    :maxdepth: 3
    :caption: Contents:

    optilog/installation.rst
    optilog/enduser.rst
    optilog/solverdeveloper.rst
    optilog/use-cases.rst
    optilog/references.rst
    optilog/changelog.rst
    optilog/license.rst


..
    Indices and tables
    ==================

    * :ref:`genindex`
    * :ref:`modindex`
    * :ref:`search`