3-SAT和CNF之间的差异

Question

我试图用Z3定理求解器解决SMT-LIB语法中的SAT问题，我要求在CNF中编写命题公式并找到令人满意的值。我知道这些概念，但不了解实现。你们能举一个Z3定理证明者解决3-SAT问题的例子吗。谢谢

Answer 1

DIMACS格式的3-SAT CNF输入文件示例：

文件xor.txt:

p cnf 3 4
1 2 3 0
1 -2 -3 0
-1 2 -3 0
-1 -2 3 0

要找到这个连接范式的解决方案，请调用z3:

z3 -dimacs xor.txt

命令行参数-dimacs通知Z3关于输入格式的信息。

结果输出：

sat
1 -2 -3

这意味着问题对于的解是可满足的

Variable 1 true
2 false
3 false

3-SAT将CNF限制为每个文本不超过三个的子句。

要将命题公式转换为CNF，可以使用bc2cnf等工具。