减少以下问题坐下

Question

这是问题。给定$ k，n，t_1， ldots，t_m $，其中$ t_i subseteq {1， ldots，n } $。是否有一个子集$ s subseteq {1， ldots，n } $，最多是$ k $，以便所有$ i $的$ s cap t_i neq neq emptyset $？我试图减少坐此问题。我的解决方案的想法是要为1至$ n $中的每个中的每个$ x_i $。对于每个$ t_i $，创建一个子句$（x_ {i_1} vee cdots vee x_ x_ {i_k}）$如果$ t_i = {i_1， ldots，i_k } $。然后以及所有这些子句在一起。但这显然不是一个完整的解决方案，因为它不能代表$ s $最多必须具有$ k $元素的约束。我知道我必须创建更多变量，但我根本不确定如何。所以我有两个问题：

1. 我在正确的轨道上解决方案的想法吗？
2. 如何创建新变量，以便可以用来表示基数$ k $约束？

Answer 1

看起来您正在尝试计算 超图形横向 大小$ k $。也就是说，$ {t_1， dots，t_m } $是您的超图，$ s $是您的横向。标准翻译是表达您的子句，然后将长度限制转换为基数约束。

So use your existing encoding, ie, $bigwedge_{1 le j le m} bigvee_{i in T_j} x_i$ and then add clauses encoding $sum_{1 le i le n} x_i le K $。

$ sum_ {1 le i le n} x_i le k $是基数约束。 SAT有各种不同的基数约束翻译。

最简单但相当大的心脏约束翻译只是$ bigWedge_ {x subseteq {1， dots，n }，| x | = k+1} bigVee_ {i in x} neg x_i $。这样，每个分离代表约束$ neg neg bigwedge_ {i in x}} x_i $ - 对于所有子集$ x $ of $ {1， dots， dots，n } $ size k+1的$。也就是说，我们确保无法设置K变量超过更多的方法。 请注意，这不是$ k $中的多项式大小

一些链接指向更高空间效率的基数约束翻译的论文链接 $ k $中的多项式大小:

• 将伪树状约束转换为SAT -NiklasEén和NiklasSörensson，JSAT第2卷（2006年），第1-26页（一项很好的调查）。
• 布尔基数约束的有效CNF编码 -Olivier Bailleux和Yacine Boufkhad，《 2003年约束编程原则和实践论文集》，LNCS第2833卷，第108-122页（一个很好，易于实现的翻译）。
• 达到布尔基数约束的最佳CNF编码 -Carsten Sinz- 2005年约束编程原则和实践论文集，LNCS 3709，第827-831页。
• 朝着强大的CNF编码基础限制 -Joao Marques-Silva和InêsLynce，《 2007年约束计划原则和实践论文集》，LNCS 4741，PG 483-497。

如果您实际上对解决此类问题感兴趣，也许最好将它们作为伪树立问题（请参阅 Wiki关于伪树立问题的文章）并使用伪树状求解器（请参阅 伪树立竞赛）。这样一来，基数约束只是伪树状的约束，并且是语言的一部分 - 希望伪树状求解器然后直接处理它们，因此可以更有效地处理它们。

Answer 2

如果您不是绝对设置在正常的SAT上，那么您的想法已经减少到Min-on-on-on-on-on-on-on-on-on-on-offor（正是CNF公式），这基本上是SAT，但是您可以将最多设置为$ k $变量为true（严格来说是的我们最大程度地减少真实变量的数量的优化版本。

同样，如果您朝着参数化的复杂性方向前进，那么您基本上已经获得了wsat（$ gamma_ {2,1}}^{+} $），其中$ gamma_ {2,1}^{+} $是所有积极的CNF公式的类别（与以前相同，符号可能有助于您的调查）。在这种情况下，您必须开始查看哪些参数化对您的情况有用。

我认为您正在寻找明确的减少，但是如果没有，您总是可以回到 Cook-Levin定理.