问3-SAT和CNF之间的差异

EN

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

文件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这样的工具。