algorithm - 2 可满足性强连通分量拓扑排序

Question

我正在用 SCC 解决一个双可满足性问题，并且有一个关于拓扑排序的问题。我基于此的算法是以反向拓扑顺序处理 SCC，当它们全部连接时这很好。我的算法在这种情况下出现问题:

3 3
-2 3
1 -2
-2 -1

这使得图表看起来像这样:

此图中有两个源和两个汇，根据您从哪里开始，有多种拓扑排序，因此有两个可能的最终节点。没有循环，所以每个节点都是一个 SCC。从源到接收器有多条路径，因此当我进行反向拓扑顺序时，我可以从接收器 x3 或接收器 !x2 开始。给我正确答案的路径是从 !x2 开始，这将导致 1、-2、-3 或 -1、-2、-3，这两个都是解决方案。但是，如果我从 x3 开始，一个可能的结果是 -1、2、3，这不是解决方案。

所以当我查看我的两个水槽时，我如何从拓扑上决定哪个在最后？显然答案是 !x2，但我试图弄清楚算法将如何确定它。我看到四种可能的想法:

• !x2 是最后一个，因为它有更多节点通向它
• !x2 是最后一个，因为它在较长路径的尽头
• 在我开始处理任何事情之前设置每个接收器的真值
• 无法知道哪个是最后一个，因此请创建所有可能的解决方案并测试每个解决方案以查看其是否有效。

或者是否有关于拓扑排序 SCC 的内容我没有讲到这里？这是基于我在之前的类(class)中通过强连通分量作业时使用的算法，因此不会完全错误。

Answer 1

在没有看到您的代码的情况下，我无法确定，但我的猜测是，当您处理文字时，您正在设置一个值，然后当您在拓扑顺序中更深地遇到它的否定时将其翻转。关键是一旦你设置了一个变量，你就不会再改变它。跳过任何已经具有设定值的变量的文字。

编辑添加:从您的评论中我想我看到了问题。当 !x2 在反向拓扑排序中排在第一位时，您提到将变量 x2 设置为 true 。您应该将 literal !x2 设置为 true，这意味着您将 variable x2 设置为 false。如果您这样做，那么无论您从哪个汇开始，您的求解器都应该工作。