如何估计在 z3 中用于 SMT 的 SAT 求解部分所花费的时间? [英] How to estimate time spent in SAT solving part in z3 for SMT?

问题描述

我已经使用分析器 gprof (stats 此处 包括调用图)并试图将花费的时间分为两类:

I have profiled my problems, which are in (pseudo-nonlinear) integer real fragment using the profiler gprof (stats here including the call graph) and was trying to separate out the time taken into two classes:

I) SAT 解决部分(包括 [纯] 布尔传播和 [纯] 布尔冲突从句检测、回跳、任何其他命题操作)

I)The SAT solving part (including [purely] boolean propagation and [purely] boolean conflict clause detection, backjumping, any other propositional manipulation)

II) 理论求解部分(包括理论一致性检查、理论冲突条款的生成和理论传播).

II)The theory solving part (including theory consistency checks, generation of theory conflict-clauses and theory propagation).

在 smt_context.cpp 内执行第 3280-3346 行bounded_search() 构成顶层DPLL(X)循环?

Do lines 3280-3346 in smt_context.cpp within bounded_search() constitute the top-level DPLL(X) loop?

我相信在 SAT 求解器函数中总结时间更容易(因为它们更少)然后剩下的可以被认为是理论求解者的时间.我想弄清楚我应该考虑哪些功能属于上述 I 类?它们是 smt::context::decide(), smt::context::bcp() 在 smt::context::propagate() 内吗?代码>?还有其他人吗?smt::context: resolve_conflict() 似乎与对理论求解器的调用混合在一起?

I believe it is easier to sum-up the time in SAT solver functions (since they are fewer) and then the rest can be considered as theory solvers's time. I am trying to figure out which functions I should consider as falling under class I above? Are they smt::context::decide(), smt::context::bcp() within smt::context::propagate()? Any others? smt::context: resolve_conflict() seems to be mixed with calls to theory solver?

smt::context::propagate() 除了它的 bcp() 函数似乎主要是理论传播(第二类)是否正确?此外，smt::context::final_check() 似乎纯粹属于 II 类.

Is it correct that smt::context::propagate() seems to be mostly theory propagation (class II) except its bcp() function? Also, smt::context::final_check() seems to be purely in class II.

非常感谢任何提示.谢谢.

Any hints greatly appreciated. Thanks.

推荐答案

你说得对，bcp() 和 decide() 是SAT 求解器"的一部分.函数 final_check() 只是理论推理.它执行Z3声称"太昂贵"的程序.resolve_conflict() 过程是混合的:它执行引理学习和回溯.为了生成新引理，Z3 使用布尔解析(在SAT 部分"中).在某些情况下，resolve_conflict 最昂贵的部分是回溯理论求解器的状态.

You are correct, bcp() and decide() are part of the "SAT solver". The function final_check() is just theory reasoning. It executes procedures that Z3 "claims" to be too "expensive". The resolve_conflict() procedure is mixed: it performs lemma learning, and backtracking. To generate new lemmas, Z3 uses Boolean resolution (which is in "SAT part"). In several cases, the most expensive part of resolve_conflict is backtracking the state of the theory solvers.

这篇关于如何估计在 z3 中用于 SMT 的 SAT 求解部分所花费的时间?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！