SBV库对于SAT的解决似乎比较慢，如何使用picosat/miniSAT？

Question

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

不幸的是，SBV似乎不适合于相当快的SAT求解，或者"allSat“函数找出所有的模型没有实现的速度。毕竟，SBV的目标是解决SMT问题。

与picosat相比，我使用Z3和CVC4测试了haskell包的性能。我使用了一个包含36个变量和840个有效模型的命题公式。picosat的结果是它花了0.5秒，而Z3花了3分钟，CVC4花了6分钟。或者有一些关于SBV和"allSat“函数的性能技巧来修饰它的命题公式。或者其他一些测试工具可能比Z3更快。

但我现在认为我可能需要使用一个更快的选项来解决SAT，我想使用PicoSAT或MiniSAT，因为我在过去有好的成绩，而SAT竞赛的结果似乎很好。

问题：

• 是否有一个与Picosat或MiniSAT的绑定，适合于找到一个命题公式的所有模型(即C/C++级别上的快速结果)？例如，python绑定到picosat的功能就是这样做的“迭代解决”函数。但是，我无法为haskell或miniSAT绑定找到这个函数(也许我忽略了它们)。
• 我应该如何从使用hatt包解析的字符串转到适合picosat/miniSat的"int list“。因此，从hatt库中的Expr类型表达式转换为适合于例如picosat的样式的CNF公式。Picosat使用了ints列表的常见SAT格式。请注意，我从字符串中解析的公式最初已经在CNF中了。要么我直接从hatt Expr转到int列表。否则，我使用从我的最后一个问题到适合SBV的allSat函数的格式的代码，并重新实现SBV的allSAT函数的一个变体，以使用picosat/miniSAT的hasekll绑定。

链接：

• 我的最后一个问题
• SBV库
• hatt图书馆
• haskell picosat绑定
• minitSAT

Answer 1

正如我在评论中所说的，一个非常常见的解决方案是通过显式添加一个子句dis来迫使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 []