Download
language Essence 1.3

$ This is the decision version of the cover test problem

given t : int(1..) $ strength (size of subset of rows)
given k : int(1..) $ rows
given g : int(2..) $ number of values
given b : int(1..) $ columns

where k>=t, b>=g**t

$ TODO:
$ - Look into the second model from https://link.springer.com/content/pdf/10.1007/s10601-006-7094-9.pdf
$ - Can we break the symmetry via unnamed types?

$ k * b of 1..g
find CA: matrix indexed by [int(1..k), int(1..b)] of int(1..g)

such that
    forAll rows : sequence (size t) of int(1..k) .
        (forAll i : int(2..t) . rows(i-1) < rows(i)) ->
        forAll values : sequence (size t) of int(1..g) .
            exists column : int(1..b) .
                forAll i : int(1..t) .
                    CA[rows(i), column] = values(i)

$ row & col symmetry breaking
such that forAll i : int(2..k) . CA[i-1,..] <=lex CA[i,..]
such that forAll i : int(2..b) . CA[..,i-1] <=lex CA[..,i]

$ =============================================================================
$ EXAMPLE
$ g=2 values
$ k=5 rows
$ b=10 columns
$ any subset of t=3 rows selected will contain all full-factorial assignments
$ 0   0   0   0   0   1   1   1   1   1
$ 0   0   0   1   1   0   0   1   1   1
$ 0   0   1   0   1   0   1   0   1   1
$ 0   1   0   0   1   0   1   1   0   1
$ 0   1   1   1   0   1   0   0   0   1

$ =============================================================================
$ INSTANCES
$
$ Note: These are all easy in that they can be solved by MiniZinc in under 2 minutes.
$       The paper cited below uses Ilog Solver, which is tens of times faster.
$
$ These are easy and unsat
$ letting t be 3, g be 2, k be 5, b be 8
$ letting t be 3, g be 2, k be 5, b be 9
$ letting t be 3, g be 2, k be 6, b be 8
$ letting t be 3, g be 2, k be 6, b be 9
$ letting t be 3, g be 2, k be 6, b be 10
$ letting t be 3, g be 2, k be 7, b be 8
$ letting t be 3, g be 2, k be 7, b be 9
$ letting t be 3, g be 2, k be 8, b be 8
$ letting t be 3, g be 2, k be 8, b be 11
$ letting t be 3, g be 2, k be 9, b be 11
$ letting t be 3, g be 2, k be 10, b be 11
$ letting t be 3, g be 2, k be 11, b be 11
$ letting t be 3, g be 2, k be 12, b be 11
$
$ These are easy and sat
$ letting t be 3, g be 2, k be 4, b be 8
$ letting t be 3, g be 2, k be 4, b be 9
$ letting t be 3, g be 2, k be 5, b be 10
$ letting t be 3, g be 2, k be 6, b be 12
$ letting t be 3, g be 2, k be 7, b be 12
$ letting t be 3, g be 2, k be 8, b be 12
$ letting t be 3, g be 2, k be 9, b be 12
$ letting t be 3, g be 2, k be 10, b be 12
$ letting t be 3, g be 2, k be 11, b be 12