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

Question

今天我也想看看在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解算器.在我受过良好教育的猜测中,我是否正确,对于简单的SAT解决而言,picosat比Z3更快？

Answer 1

披露,我是你提到的Haskell picosat绑定的作者.

SBV是一个非常强大的库,已经存在了一段时间,如果你想要一个外部SMT或SAT求解器(如Yices或Z3)的接口,这是很好的.Picosat是一个更简单的库,我写的只是因为我想要一个可以安装简单而没有外部依赖的库.

在我受过良好教育的猜测中,我是否正确,对于简单的SAT解决而言,picosat比Z3更快？

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

Answer 2

SBV是线程安全的.

比较Z3和Lingeling的SAT性能并非易事.我猜测它们或多或少会相同,除非你花时间找出精确的参数来微调它们的内部启发式.

好处是SBV提供了一个通用接口,因此您可以通过仅导入不同的桥来更改求解器:

import Data.SBV.Bridge.Z3

VS

import Data.SBV.Bridge.Boolector

如果你编译boolector来使用lingeling,那么只需更改一行Haskell就可以轻松测试性能.