sat - 哪个工具最适合转换 CNF（甚至更好的 DIMACS CNF）中的子句？

Question

我使用 C++ 程序自动生成这样的子句：

((((((condition1#0 and not action1#0 and not action2#0 and TRUE) and (action1#1 and not action2#1 and not condition1#1 and TRUE) and TRUE)) or (not action1#0 and not action2#0 and not condition1#0 and action2#1 and not action1#1 and not condition1#1 and TRUE) or FALSE)))

然后我需要用一些工具（比如 MiniSat）检查它们的可满足性，但是在将它们输入这样的工具之前，我需要在 DIMACS CNF 中转换它们，你知道有什么工具可以自动为我完成吗？

谢谢！

编辑：

非 CNF sat 求解器也可以正常工作！

Answer 1

在 pysmt 中有一个称为人类可读解析器 (hrparser) 的解析器应该能够解析这些表达式。[1] 。

Pysmt 与 picosat 和 cudd bdd 包集成，因此您可以轻松检查可满足性。一般来说，smt求解器在输入（非cnf）的结构上更加灵活。如果您可以更改 c++ 代码的输出，那么创建 smtlib 文件并使用 smt silver（例如 yices、z3 或 cvc4）可能很容易。

注意：我是 pysmt [1] http://pysmt.readthedocs.io/en/latest/_modules/pysmt/parsing.html#HRParser的开发者之一