0

我想通过 SBV 使用多核使用 Z3。基于这个答案，我应该能够通过在命令行上传递给可执行文件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 并行化？

4

1 回答 1

2

您所做的基本上是从 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_outputcreated 在当前目录中的文件，其中包含以下几行：

(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 并发运行事物的组合器。查看函数：

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

于 2020-07-30T14:38:20.980 回答