使用Z3与SBV并行化

Question

我想使用Z3通过SBV使用多核。基于这个答案 --我应该能够通过将parallel.enable=true传递给命令行中的z3可执行文件来做到这一点。由于我使用的是SBV，所以我需要通过SBV与各种SMTLib解决程序的接口，下面是我所尝试的：

foo = runSMTWith z3par $ do
    ...
  where
    z3par = z3
        { SBV.solver = (SBV.solver z3)
              { SBV.options = \cfg -> SBV.options (SBV.solver z3) cfg ++ ["parallel.enable=true"]
              }
        }

但是，我没有看到任何Z3运行时启用并行化的迹象：

• CPU使用率不会超过一个核心
• 与没有此标志的运行相比，没有加速。

当通过SBV时，如何启用Z3并行化？

Answer 1

从本质上讲，你所做的是如何从SBV实现的。您可能希望增加z3的详细性，并将诊断结果输出到一个文件中，以便稍后进行检查。类似于：

import Data.SBV
import Data.SBV.Control

foo :: IO (Word64, Word64)
foo = runSMTWith z3{solver = par} $ do
        x <- sWord64 "x"
        y <- sWord64 "y"

        setOption $ DiagnosticOutputChannel "diagnostic_output"

        constrain $ x * y .== 13
        constrain $ x .> 1
        constrain $ y .> 1

        query $ do ensureSat
                   (,) <$> getValue x <*> getValue y

  where par    = (solver z3) {options = \cfg -> options (solver z3) cfg ++ extras}
        extras = [ "parallel.enable=true"
                 , "-v:3"
                 ]

在这里，我们不仅设置了z3的并行模式，还告诉它增加详细信息，并将所有诊断信息放在一个文件中。(附带注意:在z3配置的并行部分中还有许多其他设置，您可以通过在命令行中发出z3 -pd并查看输出来查看它们是什么。可以通过将其添加到上面的extras变量来设置其他参数。)

当我运行上面的内容时，我得到：

*Main> foo
(6379316565415788539,3774100875216427415)

但是，我还在当前目录中创建了一个名为diagnostic_output的文件，其中包含以下行：

(tactic.parallel :progress 0%  :open 1)
(tactic.parallel :split-cube 0)
(parallel.tactic simplify-1)
(tactic.parallel :progress 100.00% :status sat :open 0)

因此，z3确实处于并行模式，事情正在发生。当然，它的确切功能或多或少是一个黑匣子，如果不检查z3内部结构，就不可能解释上面的输出。(我不认为这些统计数据的含义和并行求解器的策略都有很好的文档记录。如果你找到一份关于细节的好文件，请报告！)

更新

对于这个提交，您现在可以简单地说：

runSMTWith z3{extraArgs = ["parallel.enable=true"]} $ do ...

进一步简化编程。

直接从SBV中求解无关的并发性

请注意，SBV还具有直接从Haskell并发运行事物的组合器。见以下职能：

• satConcurrentWithAny
• satConcurrentWithAll
• proveConcurrentWithAny
• proveConcurrentWithAll

这些功能是不可知的，你可以和你选择的任何解决者一起使用它们。当然，它们要求您重新构造您的问题，并进行手动分解，以利用计算机中的多核，并自己将解决方案缝合在一起。但它们也能让你完全控制你想要如何组织昂贵的搜索。