今天我也想研究一下在 haskell 中解决 SAT 的选项。首先，我想为 picosat 求解器编写自己的界面。
然后我发现那里有SBV 库。它是 Z3、Yices、CVC4 和 Boolector 的接口。
此外，我在 github 上进行了谷歌搜索，结果发现甚至有可用的Picosat 绑定。
考虑到快速/高性能的限制，是否有任何其他与 SAT 求解器相关的 Haskell 绑定值得关注。Carification：适用于高性能 SAT 解决（例如，运行数天的问题，以及需要尽快完成的问题，因为我检查了 2^20 或更多 SAT 问题）。例如，我在 hackage 中特别缺少的是与 Plingeling 等快速并行 SAT 求解器的绑定。（另外，我偶然发现了 github 上当前更新的 picosat 绑定，我很可能会错过其他选项）
SBV 库的默认选项是 Z3 SMT 求解器。我的有根据的猜测是否正确，即 picosat 比 Z3 更快地解决普通 SAT 问题？
披露，我是你提到的 Haskell picosat 绑定的作者。
SBV 是一个非常强大的库，已经存在了一段时间，如果您想要一个与 Yices 或 Z3 等外部 SMT 或 SAT 求解器的接口，那就太好了。Picosat 是一个简单得多的库，我之所以编写它只是因为我想要一个无需外部依赖即可轻松安装的库。
我的有根据的猜测是否正确，即 picosat 比 Z3 更快地解决普通 SAT 问题？
我不知道你的性能限制是什么，但就底层求解器库而言，在你遇到真正巨大的问题（数十亿个变量）之前，你不会注意到 Z3 或 Picosat 之间的显着差异。两者都是非常优化的库，瓶颈（至少从 Haskell 方面）很可能是在库和 Haskell 的运行时之间编组数据。
SBV 是线程安全的。
比较 Z3 和 Lingeling 的 SAT 成绩并非易事。我冒险猜测它们或多或少是相同的，除非您花时间找出确切的参数来微调它们的内部启发式。
好消息是 SBV 提供了一个通用接口，因此您只需导入不同的桥即可更改求解器：
import Data.SBV.Bridge.Z3
对比
import Data.SBV.Bridge.Boolector
如果你编译 boolector 以使用 lingeling，那么你可以通过仅仅改变 Haskell 的一行来轻松测试性能。