z3 - 如何估计在 z3 for SMT 中解决 SAT 部分所花费的时间？

Question

我已经使用探查器 gprof(统计 here 包括调用图)分析了我的问题，这些问题位于(伪非线性)整数实数片段中，并试图将所花费的时间分为两类:

I)SAT 求解部分(包括[纯粹] bool 传播和[纯粹] bool 冲突子句检测、回跳、任何其他命题操作)

II)理论求解部分(包括理论一致性检验、理论冲突子句生成和理论传播)。

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

我相信总结 SAT 求解器函数的时间会更容易(因为它们更少)然后剩下的时间就可以视为理论求解者的时间了。我想弄清楚哪些函数应该属于上面的 I 类？他们是smt::context::decide() , smt::context::bcp() smt::context::propagate()内？还有其他人吗？ smt::context: resolve_conflict()似乎与理论求解器的调用混合在一起？

smt::context::propagate() 是否正确？似乎主要是理论传播(II 类)，除了它的 bcp()功能？另外，smt::context::final_check()看来纯粹是II类的。

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

Answer 1

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