CALOT

The CALOT algorithm encodes the 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 [YKA+15].

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

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

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