Haskell:绑定(bind)到快速且简单的 SAT 求解器

Question

今天我也想研究一下 Haskell 中 SAT 求解的选项。首先，我考虑编写自己的 picosat 求解器接口(interface)。

然后我发现有SBV library 。它是 Z3、Yices、CVC4 和 Boolector 的接口(interface)。

此外，我在 github 上进行了谷歌搜索，结果发现甚至有 Picosat binding可用。

考虑到快速/高性能的限制，是否有任何其他与 SAT 求解器的 haskell 绑定(bind)值得考虑。 Carification:同样适合高性能 SAT 解决(例如，运行数天的问题，以及需要尽快完成的问题，因为我检查了 2^20 或更多 SAT 问题)。例如，我在 hackage 中特别缺少的是与快速并行 SAT 求解器的绑定(bind)，如 Plingeling 。 (另外，我更偶然地在 github 上发现了当前更新的 picosat 绑定(bind)，我很可能会错过其他选项)

SBV 库的默认选项是 Z3 SMT 求解器。我的猜测是否正确，即 picosat 的普通 SAT 求解速度比 Z3 更快？

Answer 1

披露，我是您提到的 Haskell picosat 绑定(bind)的作者。

SBV 是一个非常强大的库，已经存在了一段时间，如果您想要一个与外部 SMT 或 SAT 求解器(如 Yices 或 Z3)的接口(interface)，它会很好。 Picosat 是一个简单得多的库，我编写它只是因为我想要一个无需外部依赖即可简单安装的库。

Am I right in my educated guess that picosat is faster for plain SAT-solving than Z3?

我不知道你的性能限制是什么，但就底层解算器库而言，你不会注意到 Z3 或 Picosat 之间的显着差异，直到你遇到真正巨大的问题(数十亿个变量)。两者都是经过高度优化的库，瓶颈(至少在 Haskell 方面)很可能是在库和 Haskell 运行时之间编码数据。