【发布时间】：2014-01-22 11:56:32
【问题描述】：
今天我也想研究一下在 haskell 中解决 SAT 问题的选项。首先，我决定编写自己的 picosat 求解器接口。
然后我发现有SBV library。 它是 Z3、Yices、CVC4 和 Boolector 的接口。
另外，我在 github 上进行了谷歌搜索，结果发现甚至有 Picosat binding 可用。
考虑到快速/高性能的限制，是否有任何其他与 SAT 求解器相关的 Haskell 绑定值得研究。 Carification：适用于高性能 SAT 解决（例如，运行数天的问题，以及需要尽快完成的问题，因为我检查了 2^20 或更多 SAT 问题）。例如，我在 hackage 中特别缺少的是绑定到像 Plingeling 这样的快速并行 SAT 求解器。 （另外，我在 github 上发现了当前更新的 picosat 绑定更多的是偶然，我很可能会错过其他选项）
SBV 库的默认选项是 Z3 SMT 求解器。我的有根据的猜测是否正确，即 picosat 比 Z3 更快地解决普通 SAT 问题？
【问题讨论】：
-
不想刻薄，但你知道看看hackage吗？那里已经有很多 SAT 和 SMT 包，只需搜索“sat”就会产生 10 个包（有些是绑定，有些是管道，有些是 Haskell SAT 实现）。搜索“smt”会产生其他几个，您可能会通过四处搜寻找到一两个（例如：“picosat”正在被黑客入侵）。
-
我按类别查看了hackage并在浏览器中搜索，但显然有文本搜索功能。 hackage 的其他选项要么是 SBV 库已经提供的绑定，要么在速度方面与 picosat 没有比较。
-
Thomas，你有没有想过是否所有的 hackage 包库都适合繁琐的多线程编程？从某种意义上说，我的 SAT 问题都是严格分开的，并且不需要共享内存左右，我只想一次对不同的问题进行 n SAT 调用。
-
我猜你感兴趣的库都是线程安全的。也就是说，并非所有 Hackage 软件包都如此。上传到 hackage 没有质量保证 - 您需要做的就是申请一个帐户。因此，有很多关于 hackage 的东西可能看似不是线程保存（我的最新示例是安全套接字，因为 OpenSSL 使用了线程本地存储）。
-
你说你正在处理 2^20 个问题——它们在某种程度上是否相关？也许这只是一个 QBF-SAT 问题？ fmv.jku.at/qbf2013
标签： haskell z3 smt satisfiability picosat