如何估算SAT在z3中为SMT解决部分所花费的时间？

Question

我已经使用profiler gprof(这里包括调用图的统计数据)描述了我的问题,这些问题在(伪非线性)整数实际片段中,并且试图将分成两个类的时间分开:

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

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

做线3280-3346在smt_context.cpp内bounded_search()组成的顶级DPLL(X)循环？

我相信在SAT求解器函数中总结时间更容易(因为它们更少),然后其余的可以被认为是理论解算器的时间.我想弄清楚我应该考虑哪些功能属于上面的I类？他们是smt::context::decide(),smt::context::bcp()内smt::context::propagate()？还有其他人？ smt::context: resolve_conflict()似乎与理论解决者的呼吁混在一起？

它的功能smt::context::propagate()似乎主要是理论传播(第二类)bcp()吗？而且,smt::context::final_check()似乎纯粹是在II级.

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

Answer 1

你是对的,bcp()并且decide()是"SAT求解器"的一部分.这个功能final_check()只是理论推理.它执行Z3"声称"过于"昂贵"的程序.该resolve_conflict()程序是喜忧参半:它执行引理学习,并回溯.为了生成新的引理,Z3使用布尔分辨率(在"SAT部分"中).在一些情况下,最昂贵的部分resolve_conflict是回溯理论解决者的状态.