solver - SAT 求解器如何生成模型（assignment[s]）？

Question

这是一个非常简单的cnf实例，如(x1 or x2 or x3)&(x1 or x2)&(x2 or x3)，公式绝对可以满足，解x1 = x2 = x3 = 1，就够了。那么，我的问题是求解器如何使用 DPLL 或其他程序生成分配？谢谢。

Answer 1

好吧，基本上，对于 CDCL 的情况

（CDCL SAT 求解器实现 DPLL，但可以学习新的子句并不按时间顺序回溯。使用冲突分析的子句学习不会影响完整性或完整性。冲突分析使用解析操作识别新子句。因此每个学习的子句都可以从原始子句中推断出来子句和其他学习子句通过一系列解析步骤。如果 cN 是新学习的子句，则 φ 是可满足的当且仅当 φ ∪ {cN} 也是可满足的。此外，修改后的回溯步骤也不影响可靠性或完整性，因为回溯信息是从每个新学习的子句中获得的。）。（来源：维基百科）

它的工作方式如下：

首先选择一个分支变量 x1。黄色圆圈表示任意决定。

现在应用单元传播，这会产生 x4 必须为 1（即 True）。灰色圆圈表示单元传播期间的强制变量分配。结果图称为蕴涵图。

任意选择另一个分支变量 x3。

应用单元传播并找到新的蕴涵图。

这里变量 x8 和 x12 被强制分别为 0 和 1。

选择另一个分支变量 x2。

查找蕴涵图。

选择另一个分支变量 x7。

查找蕴涵图。

发现冲突！

找到导致这种冲突的切入点。从切口中，找到一个冲突的条件。

取这个条件的否定，使它成为一个子句。

将冲突子句添加到问题中。

非按时间顺序返回到适当的决策级别。

向后跳转并相应地设置变量值。

（完全来自维基百科的答案：Conflict-Driven_Clause_Learning#Example）

这是使用 CDCL 算法的求解器的列表（不确定），您应该查看它们：

• 迷你卫星。
• 扎夫SAT。
• Z3。
• 许多SAT。