将 Z3 与 SBV 的并行化一起使用答案

【问题标题】：Using Z3 with parallelization from SBV将 Z3 与 SBV 的并行化一起使用
【发布时间】：2020-11-19 21:44:03
【问题描述】：

我想通过 SBV 使用多核 Z3。 Based on this answer 我应该可以通过将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 并行化？

【问题讨论】：

标签： haskell z3 sbv

【解决方案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 内部，就不可能解释上述输出。（我认为这些统计数据的含义和并行求解器的策略都没有很好的文档记录。如果您找到有关详细信息的良好文档，请报告！）

更新

从commit 开始，您现在可以简单地说：

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

进一步简化编程。

直接从 SBV 求解不可知的并发

请注意，SBV 还具有用于直接从 Haskell 并发运行事物的组合器。查看函数：

这些函数与求解器无关，您可以将它们与您选择的任何求解器一起使用。当然，它们需要您重新构建问题并进行手动分解，以利用计算机中的多核并自己将解决方案拼接在一起。但它们也让您可以完全控制如何构建昂贵的搜索。

【讨论】：