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 mcac algorithms run CalotAlgorithm sut.acts 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:

Test suite size: 21
c T: OS,Pl,Re,Or
c T: L,C,K,L
c T: L,F,F,L
c T: L,F,H,L
c T: L,C,W,L
c T: W,F,K,L
c T: W,C,F,L
c T: W,C,H,L
c T: W,C,W,L
c T: M,S,K,L
c T: M,C,F,L
c T: M,F,H,L
c T: M,S,W,L
c T: i,S,F,P
c T: i,A,H,P
c T: i,F,W,P
c T: A,A,F,L
c T: A,F,H,P
c T: A,C,W,P
c T: i,S,H,L
c T: i,C,W,L
c T: i,A,W,P
Finished output of test cases. 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.

Warning

This algorithm certifies the optimality of the returned MCAC, so it is more resource-expensive than other anytime algorithms such as IPOG.

In general, we recommend its usage in small SUT models or using strength equals to 2.