haskell - 将 Z3 与 SBV 的并行化一起使用
问题描述
我想通过 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 并行化?
解决方案
您所做的基本上是从 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
created 在当前目录中的文件,其中包含以下几行:
(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 并发运行事物的组合器。查看函数:
这些函数与求解器无关,您可以将它们与您选择的任何求解器一起使用。当然,它们需要您重新构建问题并进行手动分解,以利用计算机中的多核并自己将解决方案拼接在一起。但它们也让您可以完全控制如何构建昂贵的搜索。
推荐阅读
- python - 创建包含特定列中条目的列表
- javascript - React Native 版本不匹配 - APK 有效,aab 无效
- join - kylin 是否更新连接表上的聚合
- php - 如何在表格的开头添加新行而不是在底部添加?
- javascript - React - 在完全不同的组件上调用 setState 时输入失去焦点
- java - 错误:不兼容的类型:
无法转换为 BaseOnTabSelectedListener - javascript - 如何在 react.js 中使用锚 id 标签历史
- excel - 从一个工作表中提取数据到另一个工作表
- android - 如何更新 React Native 应用程序的性能?
- android - Microsoft SpeechSDK STT 在 Android 中没有阿拉伯语语音识别