SBV-lib似乎对SAT求解速度较慢，如何使用picosat/miniSAT

Question

在我的最后一个问题中，我问如何在SBV库的帮助下解析命题表达式，然后找到公式的所有模型。我使用了hatt库来解析布尔表达式。

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

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

但我现在认为，我可能需要使用更快的SAT解决方案，我想使用PicoSAT或MiniSAT，因为我过去的成绩很好，SAT比赛的成绩似乎也很好。

问题：

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

• 我应该如何从使用hatt包解析的String继续到可用于picosat/miniSat的"int list"。因此，从hatt库中的Expr类型的表达式到以适合于例如picosat的风格表示CNF公式。Picosat使用int列表的通用SAT格式。请注意，我从字符串中解析的公式最初已经在CNF中了。要么我直接从hatt-Expr转到int列表。或者，我使用上一个问题中的代码，将其格式化为适合SBV的allSat函数，并重新实现SBV allSAT函数的变体，以使用picosat/miniSAT的hasekll绑定。

链接：

• 我的最后一个问题
• SBV库
• 哈特图书馆
• haskell-picosat绑定
• 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 []

在上面的例子中，我们有一个到solveAll的CNF输入。当发现一个解决方案时，我们通过添加对当前解决方案的否定作为新子句来返回该解决方案和所有剩余的解决方案。解算器最终将返回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 []