Is it feasible to solve this subset cover problem with SAT solver? The problem is to find $\mathcal{S}$, a minimal collect of subsets of $\{1,\dots, 17\}$ such that the two conditions are satisfied:


if $S \subseteq \mathcal{S}$ then $|S|=6$;
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.
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.