.. include:: ../shared/configurators.rst
.. _satex-black-box:


Satex Black Box
-----------------------------------------------

The Satex BlackBox module provide utilities to run solvers from the SAT solver competitions with SAT Heritage and then parse the result.


.. py:module:: optilog.blackbox
    :noindex:

.. autoclass:: SatexBlackBox


First of all we will check out the available kissat solvers:

.. code:: python
    :number-lines:

    >>> from optilog.blackbox import SatexBlackBox
    >>> 
    >>> print(SatexBlackBox.available_solvers('kissat*'))
    ['kissat-sc2020-default:2020', 'kissat-sc2020-sat:2020', 'kissat-sc2020-unsat:2020',
    'kissat-mab:2021', 'kissat-sat_crvr_gb:2021', 'kissat-sc2021:2021', 'kissat_bonus:2021',
    'kissat_cf:2021', 'kissat_gb:2021']

Then, we can create a new SAT solver and solve a CNF instance:


.. code:: python
    :number-lines:

    >>> from optilog.blackbox import SatexBlackBox, ExecutionConstraints, DockerEnforcer
    >>> 
    >>> bb = SatexBlackBox(
    >>>     'kissat-mab:2021',
    >>>     constraints=ExecutionConstraints(
    >>>          h_wall_time=100,
    >>>          h_real_memory='100M',
    >>>          enforcer=DockerEnforcer()
    >>>     ))
    >>> 
    >>> bb.run('/path/to/instance')
    >>> 
    >>> print(bb.sat)
    SATISFIABLE
    >>> print(bb.is_sat)
    True
    >>> print(bb.model)
    [1, 2, 3, 4, ..., 99, -100]


We can do the exact same thing with a CNF formula:

.. code:: python
    :number-lines:

    >>> from optilog.blackbox import SatexBlackBox
    >>> from optilog.formulas import CNF
    >>> c = CNF()
    >>> c.add_clause([1, 2, 3])
    >>> c.add_clause([-1])
    >>> c.add_clause([-3])
    >>> 
    >>> 
    >>> bb = SatexBlackBox('kissat-mab:2021')
    >>> 
    >>> bb.run(c)
    >>> 
    >>> print(bb.sat)
    SATISFIABLE
    >>> print(bb.is_sat)
    True
    >>> print(bb.model)
    [-1, 2, -3]