.. _maxsat_its:

MaxSAT-its
==========

The MaxSAT-its is a greedy MCAC algorithm.
At each step, it builds a new test suite that tries to maximize the number of covered tuples using MaxSAT technology.
It was first described in :cite:p:`DBLP:journals/corr/abs-2105-12552`.

Notice that this algorithm can be much more time consuming than the :ref:`bot_its_main`.
An example of its execution over the SUT presented in :ref:`handson-ctlog` for strength 2 is shown below:

.. code-block:: console

    ctlog maxsat-its sut.acts -t 2

.. code-block::

    c To be covered: 82 tuples
    s OPTIMUM FOUND
    o 76
    o T:1;TCov:6;AccCov:6
    s OPTIMUM FOUND
    o 76
    o T:2;TCov:6;AccCov:12
    s OPTIMUM FOUND
    o 76
    o T:3;TCov:6;AccCov:18
    s OPTIMUM FOUND
    o 76
    ...
    o T:20;TCov:1;AccCov:68
    s OPTIMUM FOUND
    o 81
    o T:21;TCov:1;AccCov:69
    s OPTIMUM FOUND
    o 82
    c Found test with 0 coverage. Exiting.
    c T: OS,Pl,Re,Or
    c T: A,C,W,L
    c T: L,F,K,L
    c T: M,S,F,L
    c T: A,F,H,P
    c T: i,S,W,P
    c T: i,A,H,L
    c T: A,A,F,P
    c T: W,F,W,L
    c T: i,C,F,P
    c T: L,C,H,L
    c T: M,C,K,L
    c T: W,C,F,L
    c T: L,F,F,L
    c T: M,F,W,L
    c T: M,S,H,L
    c T: M,S,K,L
    c T: i,F,W,L
    c T: i,A,W,L
    c T: L,F,W,L
    c T: W,F,K,L
    c T: W,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-its algorithm see the :ref:`cli`.