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

Question

我已经使用分析器 gprof（统计 here 包括调用图）分析了我的问题，它们位于（伪非线性）整数实数片段中，并试图将时间分为两类：

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

II)理论解决部分（包括理论一致性检查、理论冲突子句的生成和理论传播）。

bounded_search() 内smt_context.cpp 中的第 3280-3346 行是否构成顶层 DPLL(X) 循环？

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

smt::context::propagate() 除了bcp() 功能之外似乎主要是理论传播（II 类），这对吗？另外，smt::context::final_check() 似乎纯粹属于 II 类。

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

Answer 1

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