使用bc2cnf生成DIMACS CNF文件时缺少AND

Question

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

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

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

这里，可以观察到没有生成AND门的正确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

CCD_ 4具有许多有用的参数。尝试bc2cnf -?以获得帮助。