使用 bc2cnf 生成 DIMACS CNF 文件丢失并且

Question

我尝试使用 bc2cnf 工具生成布尔方程的 DIMACS CNF 文件。

输入文件包含与门的方程，如下所示：

BC1.1
f := A & B;
ASSIGN f;

使用的命令： ./bc2cnf -v inp.txt opt.txt

输出文件中的内容：

c The instance was satisfiable
c A <-> T
c B <-> T
c f <-> T
p cnf 1 1
1 0

在这里，可以观察到正确的不生成与门的 DIMACS CNF 格式。

请让我知道如何纠正这个问题。

Answer 1

使用命令行参数 -nosimplify 抑制 bc2cnf 优化。

结果是

c f <-> 1
c B <-> 2
c A <-> 3
p cnf 3 4
-1 2 0
-1 3 0
1 -3 -2 0
1 0

bc2cnf 有许多有用的参数。尝试 bc2cnf -? 获取帮助。