sat - 解决多个假设

Question

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

Answer 1

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

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

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

Answer 2

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

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

优点：

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

缺点：

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

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