logic - ddcal 不工作

Question

我正在尝试使用DDcal来评估二元决策图。当我尝试评估某些公式时，例如：a+b*c'，我总是得到这个错误：

util_pipefork: can not exec dot: No such file or directory.

有谁知道我该如何解决这个错误？

感谢您的任何见解。

Answer 1

您可以使用 Python 包dd使用 Python 或 CUDD 后端处理 BDD（免责声明：我是dd的作者）。例子：

import dd.autoref as _bdd  # to use CUDD, replace `dd.bdd` with `dd.cudd`

bdd = _bdd.BDD()
bdd.declare('a', 'b', 'c')
u = bdd.add_expr(r'a \/ (b /\ ~ c)')

语法在文档中描述。如果您更喜欢写作a | (b & ~ c)，那也可以。纯 Python 后端安装了pip install dd.

您还可以使用dot（假设安装了GraphViz）进行绘图：

bdd.dump('bdd_graph.pdf')

该方法在此处BDD.dump描述。

关于DDcal的留言

grep -ilr "util_pipefork" ./*表示您从DDcal报告的错误似乎来自以下几行：

/* Set up bidirectional pipe to/from dot. */
/* A unidirectional pipe should suffice. We'll try it some day. */
retval = util_pipefork(args,&toCommand,&fromCommand,&pid);
if (retval == 0) {
(void) fprintf(stderr,"Panic: util_pipefork returned 0!\n");
exit(2);
}

因此，您需要安装GraphViz，并确保其可执行文件（特别是dot）位于运行时环境的$PATH.