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.

Note

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.

For a full example you can check Hands-on CTLog.