.. _maxsat_mcac:

MaxSAT MCAC
===========

The MaxSAT MCAC algorithm encodes the :term:`Covering Array Number problem` into a MaxSAT formula and uses a MaxSAT solver to solve the encoding.
For a more detailed description of the algorithm you can check :cite:p:`AnsoteguiIMJ13` and :cite:p:`DBLP:journals/corr/abs-2105-12552`.

This and the :ref:`calot` 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:`calot`, the MaxSAT MCAC 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 maxsat-mcac 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 MaxSAT 'ccx' ...
    c LB 18
    c UB 22
    c Elapsed time: 1s
    c Executing MaxSAT with 9997s out of 9997s
    c Solving with Linear MaxSAT
    c Not deciding over [] vars
    c Cost: 4; Best Cost: inf
    o 4
    c Cost: 3; Best Cost: 4
    o 3
    s OPTIMUM FOUND
    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,C,F,L
    c T: W,F,H,L
    c T: W,F,W,L
    c T: M,S,K,L
    c T: M,S,F,L
    c T: M,C,H,L
    c T: M,F,W,L
    c T: i,C,F,P
    c T: i,S,H,P
    c T: i,S,W,P
    c T: A,A,F,L
    c T: A,A,H,P
    c T: A,F,W,P
    c T: i,A,W,L
    c T: A,C,H,L
    c T: i,F,H,L
    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 MaxSAT MCAC algorithm see the :ref:`cli`.