MaxSAT MCAC

The MaxSAT MCAC algorithm encodes the 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 [AnsoteguiIManyaTorresJimenez13] and [AMO+22].

This and the 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 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 Hands-on CTLog for strength 2:

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 IPOG or any of the BOT-its Algorithms. The resulting output is shown below:

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 CLI Reference.