4

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)The SAT solving part (including [purely] boolean propagation and [purely] boolean conflict clause detection, backjumping, any other propositional manipulation)

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

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

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?

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.

4

1 回答 1

5

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

于 2014-01-23T19:14:03.730 回答