sat - 有没有实现非 CNF SAT 求解器的工具？

Question

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

我找不到任何东西。你能指出一个吗？

Answer 1

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

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

Answer 2

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

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

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

查看相关帖子：这里和这里

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