有没有实现非 CNF SAT 求解器的工具？答案

【问题标题】：Is there any tool that implements a non-CNF SAT solver?有没有实现非 CNF SAT 求解器的工具？
【发布时间】：2018-06-01 10:15:56
【问题描述】：

我需要一个 SAT 求解器，它不仅可以将 CNF 文件作为输入，还可以将包含命题子句的普通 txt 文件（仅用 and or 和 not 编写）。

我找不到。你能指出一个吗？

【问题讨论】：

【解决方案1】：

经过仔细搜索，我发现了limboole： http://fmv.jku.at/limboole/.

它非常有用，因为它接受任何命题逻辑公式，并且可以计算它是否有效或可满足。

【讨论】：

【解决方案2】：

看看bc2cnf，一个将布尔“电路”转换为CNF的命令行工具。

电路是布尔表达式的集合。表达式可以作为其他表达式的输入变量。

获得CNF 后，您可以将其输入SAT solver，例如cryptominisat 或Z3，以找到满足您表达方式的解决方案。

查看相关帖子：here 和 here

Simon Felix 的另一个有趣的创新是SATInterface。它允许将 C# 程序与 SAT 求解器 CaDiCaL 或 cryptominisat 耦合。

【讨论】：