寻求自动转换CNF为DIMACS CNF的工具，或支持非CNF的SAT求解器

先把你生成的逻辑子句贴出来方便后续参考：

((((((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)))

下面分两部分给你推荐实用的工具和方案：

一、自动转换非CNF到DIMACS CNF的工具 #

如果你一定要转成DIMACS格式用MiniSat这类工具，这些工具能帮你自动完成转换：

• picosat配套的picomc：这个工具可以直接处理非CNF的布尔表达式，你只需要把公式里的and换成&、not换成~、or换成|，运行对应命令就能输出标准的DIMACS CNF文件。
• SAT4J：这是个Java库，自带公式转换功能。你可以把你的表达式传入它的API，它会自动通过Tseytin转换把嵌套的与或结构转成CNF，还能直接导出DIMACS格式。
• cnfizer工具：很多SAT工具集里都附带这个小工具，它支持直接输入类似你这种的布尔表达式，自动解析并转换为DIMACS CNF，用法非常简单。

要是你想自己集成到C++程序里，也可以用boost::spirit这类解析库先解析你的公式，再手动实现Tseytin转换算法——不过这个需要点编码工作，适合需要自定义转换逻辑的场景。

二、支持非CNF公式的SAT求解器 #

如果不想折腾转换，直接用支持非CNF的求解器更高效，这些工具能直接处理你给出的复杂嵌套表达式：

• Z3 Theorem Prover：它支持C++ API，你可以直接把你的布尔表达式（用Z3的语法构造或者直接解析字符串）传进去，一键求解可满足性，完全不需要转CNF。
• CVC4：和Z3类似，是个强大的自动定理证明器，支持非CNF布尔公式的直接求解，使用起来很灵活，调试也方便。
• Yices 2：同样支持直接输入非CNF公式，求解效率不错，也有C++ API，很适合和你的自动生成程序集成。

这些工具都能完美适配你的需求，不管是转格式还是直接求解都能搞定～

内容的提问来源于stack exchange，提问作者elena