Haskell:与快速简单的SAT求解器绑定

Question

今天，我也想研究haskell的SAT解决方案。首先，我想要为picosat解决程序编写我自己的接口。

然后我发现那里有SBV库。它是Z3、Yices、CVC4和Boolector的接口。

另外，我在github上做了谷歌搜索，它甚至可以使用Picosat装订。

考虑到快速/高性能的限制，是否还有其他的haskell绑定到SAT求解器上值得考虑。认证:适用于高性能SAT解决方案(例如，持续数天的问题，以及我检查2^20或更多SAT问题时需要尽可能快完成的问题)。例如，我在hackage中特别缺少的是绑定到像平岭这样的快速并行SAT解算器。(此外，我还意外地发现了github上当前更新的picosat绑定，我很可能错过了其他选项)

SBV库的默认选项是Z3 SMT解决程序。我的猜测是正确的吗，皮科卫星对于普通SAT的解决比Z3快吗？

Answer 1

坦白说，我是你提到的Haskell picosat绑定的作者。

SBV是一个非常健壮的库，它已经存在了一段时间了，如果您想要一个外部SMT或SAT解算器的接口，比如Yice或Z3，那是很好的。Picosat是我编写的一个简单得多的库，因为我想要一个可以简单安装而不需要外部依赖的库。

我的猜测是正确的吗，皮科卫星对于普通SAT的解决比Z3快吗？

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

Answer 2

SBV是线程安全的。

比较Z3和玲玲的SAT成绩不是一件容易的事。我敢说，除非你花时间找出精确的参数来微调它们的内部启发，否则它们可能或多或少是一样的。

好的是SBV提供了一个公共接口，因此您只需导入一个不同的桥接器就可以更改求解器：

import Data.SBV.Bridge.Z3

vs

import Data.SBV.Bridge.Boolector

如果您编译boolector来使用line，那么只需更改Haskell一行就可以很容易地测试性能。