.. _calot:

CALOT
=====

The CALOT algorithm encodes the :term:`Covering Array (CA)` problem into a SAT formula and uses an incremental SAT solver to try to decrease the size of the encoded CA through a series of calls to the SAT solver.
This algorithm is based in :cite:p:`YamadaKACOB15`.

This and the :ref:`maxsat_mcac` algorithms are the only algorithms implemented in CTLog that can obtain an MCAC of optimal size.
Notice however that this migh only be achieved for smaller strengths.
As in :ref:`maxsat_mcac`, the CALOT algorithm needs an Upper Bound on the size of the MCAC.

In the following example we optimally solve the SUT presented in :ref:`handson-ctlog` for strength 2:

.. code-block:: console

    ctlog CALOT sut.acts -t 2 --ub 22

Notice how we needed to specify the Upper Bound ``--ub`` to 22.
This Upper Bound can be obtained by executing any of the greedy algorithms in CTLog, such as :ref:`ipog` or any of the :ref:`bot_its_main`.
The resulting output is shown below:

.. code-block::

    c Encoding SAT...
    c LB 18
    c UB 22
    c Elapsed time: 1s
    c Executing CALOT with 9997s out of 9997s
    c SATISFIABLE
    o 22
    c SATISFIABLE
    o 21
    c UNSATISFIABLE
    c T: OS,Pl,Re,Or
    c T: L,C,K,L
    c T: L,F,F,L
    c T: L,C,H,L
    c T: L,C,W,L
    c T: W,F,K,L
    c T: W,F,F,L
    c T: W,F,H,L
    c T: W,C,W,L
    c T: M,S,K,L
    c T: M,S,F,L
    c T: M,F,H,L
    c T: M,S,W,L
    c T: i,C,F,P
    c T: i,S,H,P
    c T: i,F,W,P
    c T: A,A,F,L
    c T: A,F,H,L
    c T: A,C,W,P
    c T: i,A,H,L
    c T: M,C,W,L
    c T: i,A,W,P
    Test suite size: 21
    Validating MCAC...
    VALIDATION OK
    Num covered: 69
    Num forbidden: 13

For a complete list of all the available parameters for the CALOT algorithm see the :ref:`cli`.