logic - 如何将一系列逻辑表达式转换/形式化为可以提供给 DPLL 算法的格式？

Question

采取以下一组逻辑语句：

A：B是假的

B：C 是假的

C：B 或 A 为真

我被赋予了将其形式化的任务，以便“DPLL”可以确定是否存在不会导致矛盾的解决方案（哪些规则是正确的，哪些是错误的）。

问题是：我不知道该怎么做。在线求解器需要某种格式的表达式，比如这里的这个：http: //www.inf.ufpr.br/dpasqualin/d3-dpll/

我如何将我的陈述转换成这些数字？

Answer 1

您可能会混淆这里的符号：我假设这里有三个语句和三个变量。我将用小写字母表示变量，用大写字母表示语句以明确这一点：

Statement A: not b
Statement B: not c
Statement C: a or b

现在用数字替换小写字母：

Statement A: not 2
Statement B: not 3
Statement C: 1 or 2

not应该写成负号，并且用or冒号代替。现在可以在您链接的 SAT 求解器中输入生成的三行：

-2
-3
1, 2

它1, -2, -3作为解决方案输出，因此变量a必须为真，b而c必须为假。