É viável resolver este problema de cobertura de subconjunto com o solucionador SAT?

Question

O problema é encontrar $\mathcal{S}$, uma coleção mínima de subconjuntos de $\{1,\pontos, 17\}$ tal que as duas condições sejam satisfeitas:

1. se $S\subseteq\mathcal{S}$ então $|S|=6$;
2. para qualquer $A \subseteq \{1,\dots,17\}$ com $|A|=3$, existe um $S\in\mathcal{S}$ com $A \subconjunto S$.

Ver aqui para um problema combinatório relacionado.

Acho que isso pode ser formulado como um problema Min SAT.

Para cada $S \subseteq \{1,\dots,17\}$ com $|S|=6$, introduzimos uma variável $X_S$.E para cada um $A \subseteq \{1,\dots,17\}$ com $|A|=3$, introduzimos uma cláusula$$ vee_ {s:A subseteq s, | s | = 6} x_ {s} $$Então, em princípio, podemos usar um solucionador SAT para encontrar o número mínimo de $X_S$ isso precisa ser verdadeiro para satisfazer todas as cláusulas.

Isso precisa $\binom{17}{6}=12376$ variáveis, $\binom{17}{3}=680$ cláusulas de comprimento $\binom{17-3}{3}=364$.

Tenho muito pouca experiência no uso de solucionadores SAT.Então, vale a pena tentar isso no meu laptop ou não há esperança alguma?

——-

Atualizar

Acontece que existem muitas pesquisas sobre cobertura de cenários.Parece que fui ambicioso demais em tentar resolver o problema dos parâmetros (17, 6, 3).

Já é um problema aberto para (12, 5, 3).

Ver aqui para mais detalhes.

———

Atualização 2

Tentei escrever tudo em SAT puro e é bastante mais rápido usando cadical do que z3.

Além disso, é significativamente mais rápido encontrar uma solução do que mostrar que não existem soluções.

Tentei quebrar a simetria adicionando as restrições de que o primeiro e o último subconjunto na ordem do léxico devem ser selecionados.

Answer 1

A otimização com SAT é geralmente referida como maxsat em vez de min sentou.Em particular, sugiro à procura de solucionadores para "MaxSat parcial ponderado", por exemplo, Maxhs e RC2.

O tamanho do problema que você tem é bastante pequeno no contexto dos modernos solucionadores MaxSat, então sim, vale a pena tentar.Não há garantias de que o solucionador funcionará eficientemente, e é muito difícil prever se funcionar de forma eficiente, então a melhor coisa a fazer é tentar.

Answer 2

Com o SAT, pode ser um desafio prever o que será viável e o que não será.Vale a tentativa.

Eu sugeriria que, em vez do MinSAT, você primeiro tentasse usar a pesquisa binária em $n=|\mathcal{S}|$, o número de conjuntos que você precisa.Você pode usar no máximo$n$-out-of-12376 restrição em seu $X_S$ variáveis.Há diversos técnicas para codificando isso no SAT, embora na prática eu primeiro tentasse usar PbLe com o solucionador Z3.

Seu problema tem muita simetria.Os solucionadores SAT às vezes podem ter dificuldade com a simetria.Você pode tentar fazer o máximo que puder para quebrar a simetria.Por exemplo, sem perda de generalidade, podemos assumir que $\{1,2,3,4,5,6\}$ é um dos conjuntos (caso contrário, permute todos os números), então você pode codificar esse fato em sua instância SAT.Quanto mais lemas você puder provar, melhor será o desempenho do solucionador SAT.

Você também pode codificar os conjuntos de maneira diferente.Deixar $S_i$ denotar o $i$o conjunto escolhido por $\mathcal{S}$.Introduzir variáveis $x_{i,j}$ para indicar que $j \in S_i$ e variáveis $y_{i,A}$ para indicar que $A \subconjunto S_i$, para cada $A \subseteq \{1,\dots,17\}$ com $|A|=3$ e cada um $i \in \{1,\pontos,n\}$ e cada um $j \in \{1,\pontos,17\}$.Adicionar uma cláusula $\bigvee_i y_{i,A}$ para cada $A$ para garantir que cada $A$ é coberto por pelo menos um conjunto.Adicione uma restrição de 6 de 17 para cada $i$ para indicar que exatamente 6 dos $x_{i,j}$são verdadeiros.Por fim, adicione restrições para reforçar a consistência entre os $x$'areia $y$'s.Em particular, para cada $A=\{a_1,a_2,a_3\}$, adicione cláusulas $ eg x_{i,a_1} \lor eg x_{i,a_2} \lor eg x_{i,a_3} \lor y_{i,A}$ e $ eg y_{i,A} \lor x_{i,a_1}$ e $ eg y_{i,A} \lor x_{i,a_2}$ e $ eg y_{i,A} \lor x_{i,a_3}$.Isso exigirá cerca $(17+680)n$ variáveis ​​e $4 \cdot 680 n$ cláusulas (sem contar as $n$ 6 de 17 restrições);já que eu espero $n \aproximadamente 35$, são cerca de 24 mil variáveis ​​e 100 mil cláusulas.São mais cláusulas do que a sua codificação e tem ainda mais simetria, por isso pode ter um desempenho pior - embora sejam cláusulas mais curtas e seja difícil prever quais codificações funcionarão melhor com SAT, muitas vezes é necessária alguma experimentação.

Você também pode tentar expressar isso como uma instância ILP em vez de SAT.