Is it feasible to solve this subset cover problem with SAT solver?

Question

The problem is to find $\mathcal{S}$, a minimal collect of subsets of $\{1,\dots, 17\}$ such that the two conditions are satisfied:

1. if $S \subseteq \mathcal{S}$ then $|S|=6$;
2. for any $A \subseteq \{1,\dots,17\}$ with $|A|=3$, there exists a $S \in \mathcal{S}$ with $A \subset S$.

See here for a related combinatorial problem..

I think this can be formulated as a Min SAT problem.

For each $S \subseteq \{1,\dots,17\}$ with $|S|=6$, we introduce a variable $X_S$. And for each $A \subseteq \{1,\dots,17\}$ with $|A|=3$, we introduce a clause $$ \vee_{S: A \subseteq S, |S|=6} X_{S} $$ Then in principal we can use a SAT solver to find the minimal number of $X_S$ that needs to be true to satisfy all the clauses.

This needs $\binom{17}{6}=12376$ variables, $\binom{17}{3}=680$ clauses of length $\binom{17-3}{3}=364$.

I have very little experience in actually using SAT solvers. So is this actually worth trying on my laptop or there's no hope at all?

——-

Update

Turn out there are many research on set covering. It seems that I was over ambitious to try to solve the problem for the parameters (17, 6, 3).

It is already an open problem for (12, 5, 3).

See here for more details.

———

Update 2

Tried to write everything in pure SAT and it’s quite a bit faster using cadical than z3.

Also, it is significantly faster to find a solution than to show no solutions exist.

I tried to break the symmetry by adding the constraints that the first and the last subset in lexicon order must be selected.

Answer 1

Optimization with SAT is usually referred as MaxSAT instead of Min SAT. In particular, I suggest looking for solvers for "weighted partial MaxSAT", for example MaxHS and RC2.

The problem size you have is fairly small in the context of modern MaxSAT-solvers, so yes it is worth trying. There are no guarantees that the solver will work efficiently, and it is very hard to predict if it will work efficiently, so the best thing to do is to try.

Answer 2

With SAT, it can be challenging to predict what will be feasible and what won't. It's worth a try.

I would suggest that, instead of MinSAT, you first try using binary search on $n=|\mathcal{S}|$, the number of sets you need. You can use an at-most-$n$-out-of-12376 constraint on your $X_S$ variables. There are several techniques for encoding that in SAT, though in practice I would first try using PbLe with the Z3 solver.

Your problem has a lot of symmetry. SAT solvers can sometimes have difficulty with symmetry. You might try to do as much as you can to break the symmetry. For instance, without loss of generality we can assume that $\{1,2,3,4,5,6\}$ is one of the sets (otherwise permute all the numbers so it is), so you might hardcode this fact into your SAT instance. The more such lemmas you can prove, the better the SAT solver might perform.

You could also encode the sets differently. Let $S_i$ denote the $i$th set that is chosen by $\mathcal{S}$. Introduce variabless $x_{i,j}$ to indicate that $j \in S_i$ and variables $y_{i,A}$ to indicate that the $A \subset S_i$, for each $A \subseteq \{1,\dots,17\}$ with $|A|=3$ and each $i \in \{1,\dots,n\}$ and each $j \in \{1,\dots,17\}$. Add a clause $\bigvee_i y_{i,A}$ for each $A$ to ensure that each $A$ is covered by at least one set. Add a 6-out-of-17 constraint for each $i$ to indicate that exactly 6 of the $x_{i,j}$'s are true. Finally, add constraints to enforce consistency between the $x$'s and $y$'s. In particular, for each $A=\{a_1,a_2,a_3\}$, add clauses $\neg x_{i,a_1} \lor \neg x_{i,a_2} \lor \neg x_{i,a_3} \lor y_{i,A}$ and $\neg y_{i,A} \lor x_{i,a_1}$ and $\neg y_{i,A} \lor x_{i,a_2}$ and $\neg y_{i,A} \lor x_{i,a_3}$. This will require about $(17+680)n$ variables and $4 \cdot 680 n$ clauses (not counting the $n$ 6-out-of-17 constraints); since I expect $n \approx 35$, this is about 24K variables and 100K clauses. That's more clauses than your encoding, and it has even more symmetry, so it might perform worse -- though they are shorter clauses, and it's hard to predict which encodings will work best with SAT, so often some experimentation is needed.

You could also try expressing this as an ILP instance instead of SAT.