解决多个假设答案

【问题标题】：Solving with multiple assumptions解决多个假设
【发布时间】：2017-02-27 21:51:23
【问题描述】：

假设我有一个带有变量 (a,b,c,d,e,f,g) 的 CNF 表达式。考虑到{a,b,c,g} = {1,0,0,1} 和{a,b,c,g} = {1,1,1,1}，我将如何使用SAT 求解器来查找(d,e,f) 的作业？如果这是一个假设，调用 sat 求解器来查找 {d,e,f} 的分配将是直截了当的（例如，通过向 CNF 添加单位子句）。但是如果我有多个假设呢？这可能吗？

【问题讨论】：

你能解释一下你的意思吗，到目前为止它看起来对我来说是微不足道的（例如 b 不能同时是 0 和 1）
假设 a,b,c,d = (1,0,0,1) 和 a,b,c,d = (1,1,1,1) 是两个“观察”。如何为 (d,e,f) 赋值以使这些观察结果一致？
那个编辑让它再次变得混乱。这是否意味着比“允许 abcg 为 1001 或 1111，无论哪个可以得到一些令人满意的模型”更复杂？还是必须对集合中的所有 abcg 向量都使用相同的 def？
很抱歉给您带来了困惑。我绝对不是指第一个（在这种情况下，您可以将它们用作阻塞子句，然后就完成了）。我的意思是 (a,b,c,d) 可以取两个值：(1,0,0,1) 和 (1,1,1,1)。当然，它也可以采用其他 (2^4 - 2) 值。但是我可以为 (d,e,f) 分配什么，以便至少满足 (a,b,c,d) 的这两个值？
但是你可以只复制 abc(d?g?) （以及所有依赖它们的子句），然后再次使用单元子句强制它们，每组副本一个分配。好的，这使得 CNF 表达式相当大.. 反正就是你的意思

标签： sat satisfiability sat-solvers

【解决方案1】：

以下是（我认为）哈罗德试图向您描述的步骤。您对变量 a、b、c、d、e、f 和 g 有一些 CNF 公式 F。

复制公式，调用复制的 G。
在 G 中，将变量 a 替换为 aa，b 替换为 bb，c 替换为 cc，g 替换为 gg。
在 F 中添加单位子句，使得 (a,b,c,g) = (1,0,0,1)。
向 G 添加单位子句，使得 (aa,bb,cc,gg) = (1,1,1,1)。
连接公式 F 和 G 并将结果输入 SAT 求解器。

求解器将找到与 (a,b,c,g) 和 (aa,bb,cc,gg) 的预设值一致的令人满意的分配。

【讨论】：

【解决方案2】：

不清楚你想要一个实际的答案还是一个有趣的理论答案。我会追求实用的。

对于每组假设，调用一个 sat 求解器，该求解器支持使用该组假设的假设进行求解 (example)。在同一个求解器实例上按顺序执行此操作。

优点：

您不要混合互斥假设集的可满足性。如果一组假设 A 满足公式 F 而另一组 A' 不满足 F，则每次调用求解器都会告诉您这些假设是否满足。
第一次调用的学习子句可能会在第二次调用中保留。中级学习从句谈论相同的变量。（注意：如果您有一个不相交的公式F & G，其中 F 在变量 X 上，G 在变量 Y 上，并且 X 和 Y 不共享变量，则分辨率（CDCL 中使用的推理规则）无法导出混合 F 和 G 的子句. 将两者混合而不是将它们分开并没有明显的好处，除非一个实例更容易证明不饱和并提前停止。）

缺点：

如果实例 A 在实践中难以解决，但 A' 微不足道，您可能会卡在 A 上。
它不是并行的，因此，如果您想要尽快解决的实例多于两个，则需要额外的机制。

我知道这是一个显而易见的答案，但值得一试。如果失败了，你可以尝试做一些更有趣的事情，比如解决 w.r.t.假设A union A'，并且只有当那是不满意的解决方案时，才回到A然后A'的这种策略。这对您的示例没有帮助，因为 (a,b,c,g) = (1,0,0,1) 和 (a,b,c,g) = (1,1,1,1) 是互斥的。

【讨论】：