haskell - SBV lib 似乎在解决 SAT 问题时变慢了，如何使用 picosat/miniSAT？

Question

在 my last question我问我如何解析一个命题表达式，然后在 SBV 库的帮助下找到公式的所有模型。我使用 hatt 库来解析 bool 表达式。

不幸的是，SBV 似乎不适合相当快速的 SAT 求解，或者查找所有模型的“allSat”功能没有实现速度。毕竟 SBV 是针对 SMT 解决的。

我使用证明器 Z3 和 CVC4 测试了 haskell SBV 包的性能，并与 picosat 进行了比较。我使用了一个包含 36 个变量和 840 个有效模型的命题公式。 picosat 的结果是用了 0.5 秒，而 Z3 用了 3 分钟，CVC4 用了 6 分钟。 SBV 和“allSat”函数有一些性能技巧可以为命题公式修剪它。或者其他一些证明器可能比 Z3 更快。

但我现在假设我可能需要使用更快的选项来解决 SAT 问题，并且我想使用 PicoSAT 或 MiniSAT，因为我过去取得了不错的成绩，而且 SAT 比赛的成绩看起来也不错。

问题:

是否存在适用于查找命题公式的所有模型(即在 C/C++ 级别以获得快速结果)的 Picosat 或 MiniSAT 绑定(bind)？例如，与 picosat 的 python 绑定(bind)具有一个功能“itersolve”，它就是这样做的。但是我找不到用于 haskell picosat 或 miniSAT 绑定(bind)的这个函数(也许我忽略了它们)。

我应该如何从使用 hatt 包解析的字符串到适用于 picosat/miniSat 的“int 列表”。因此，从 Expr 类型的表达式开始在 hatt 库中，以适合于例如 picosat 的样式表示 CNF 公式。 Picosat 使用整数列表的常见 SAT 格式。请注意，我从字符串解析的公式最初已经在 CNF 中。要么我直接从一个 hat Expr 到 int 列表。否则，我使用 my last question 中的代码为适合 allSat 的格式SBV 的函数并重新实现 allSAT 的变体SBV 的函数使用 picosat/miniSAT 的 hasekll 绑定(bind)。

链接:

my last question

SBV library

hatt library

haskell picosat bindings

minitSAT

Answer 1

正如我在评论中所说，一个非常常见的解决方案是通过显式添加禁止先前发现的解决方案的子句来强制 SAT 求解器寻找其他解决方案。例如:

solveAll :: [[Int]] -> IO [[Int]]
solveAll e =
 do s <- solve e
    case s of
        Solution x -> (x :) `fmap` solveAll (map negate x : e)
        _          -> return []

在上面我们有一个 CNF 输入到 solveAll .当发现一个解决方案时，我们通过添加我们当前解决方案的否定作为新子句来返回该解决方案和所有剩余的解决方案。求解器最终将返回 unsat，这表明我们已找到所有解决方案，或者未知，这意味着可能存在未发现的解决方案，但求解器已放弃。

一个完整的程序如下

import Data.Logic.Propositional hiding (interpret)
import Picosat
import Control.Monad ((<=<))

main :: IO ()
main = do
       let expr = [ [1, -2] , [3, -2] ]
       putStrLn $ "Solving expr: " ++ show expr
       (print <=< solve) expr
       (print <=< solveAll) expr

solveAll :: [[Int]] -> IO [[Int]]
solveAll e =
 do s <- solve e
    case s of
        Solution x -> (x :) `fmap` solveAll (map negate x : e)
        _          -> return []