Push-Pop resulting in suspicious delay in solving

[aman-goel]

Dear all,

I use Z3 C++ API for model checking of systems using QF_UF theory. I recently observed that Z3 queries were taking too long (> 1000 seconds). Further investigation resulted in the following observation.

Consider the query in file query1.smt2. The query is dumped using Z3 C++ API using to_smt2 function. When this query is run via command line using Z3 (version 4.5.1), it successfully produces the result UNSAT within 0.23 seconds.

Now consider the query in file query2.smt2 (which is a single line modified version of query1.smt2, with a (push) added once before (check-sat)). When this query is run via command line using Z3, it successfully produces the result UNSAT but takes time greater than 1000 seconds. Similar behavior is observed on similar queries irrespective of the position of (push), as long as it is before (check-sat).

Is there anything that I am missing? Can Z3 be configured to get better performance when using push-pop in solver?

Below are some details relating to the experiment:

query1.smt2 Command: z3 -st query1.smt2 Result: unsat (:added-eqs 10696 :binary-propagations 166457 :conflicts 356 :decisions 5492 :del-clause 4855 :dyn-ack 6 :max-memory 22.77 :memory 12.87 :minimized-lits 717 :mk-bool-var 30637 :mk-clause 36330 :num-allocs 12927298 :propagations 268760 :restarts 2 :rlimit-count 668855 :time 0.17 :total-time 0.23)

query2.smt2 Command: z3 -st query2.smt2 Result: unsat (:added-eqs 5722988 :binary-propagations 52279807 :conflicts 1060213 :decisions 4809725 :del-clause 559348 :dyn-ack 5 :max-memory 139.65 :memory 139.65 :minimized-lits 22329125 :mk-bool-var 30706 :mk-clause 1096294 :num-allocs 3265083377 :num-checks 1 :propagations 104028101 :restarts 1221 :rlimit-count 142326034 :time 1607.69 :total-time 1607.96)

Attachments: query1.smt2.txt query2.smt2.txt

PS: I regret that I was unable to produce a similar difference for a simpler query.

Regards Aman Goel

[martin-neuhaeusser]

I am pretty sure this behavior is due to Z3's combined solver. We have experienced similar performance degradations compared to non-incremental solving. Z3's combined solver (which is the default, I guess) internally combined a non-incremental solver which has a lot of preprocessings enabled and another solver instance which supports incrementality by the price of sacrificing many useful preprocessings.

As long as you do not use push/pop or issue multiple check-sat commands, the combined solver will use the non-incremental solver. Once the solver stack is used or you continue to assert formulas after having checked for satisfiability before, the combined solver resorts to the incremental solver.

What you can do is setting a timeout for the second (i.e. the incremental) solver. The corresponding solver parameter is called "solver2_timeout". Once the timeout expires in incremental queries, the combined solver aborts the incremental one and tries again with the non-incremental solver and an equivalent non-incremental query (where all formulas that have been asserted up to that point are asserted at once). All that is internal to Z3.

You can see more details and the code triggering the switching between solvers here

[delcypher]

@aman-goel Just to add to @martin-neuhaeusser 's reply. Until very recently this behaviour wasn't documented. You can see the new documentation on the Z3_mk_solver() function.

[aman-goel]

The suggested work-around seems to work in most cases. I have 2 further questions:

1. Would this method work for queries where unsat-core is requested?
2. Briefly, what preprocessings are we talking here that are enabled for non-incremental solver, but not in incremental solver? Could some of them be still used with incremental solver (by exploiting the domain knowledge from the type of query being asserted) by setting some parameters?

Thanks a lot for the helpful answers.

[aman-goel]

@martin-neuhaeusser @delcypher

To get a better understanding of the effect of solver2_timeout on different types of queries, I performed an experiment with a SMT2 query in QF_BV theory (query_bv.smt2). I ran 6 versions as follows:

A) Exact file, i.e. no (push), no (get-unsat-core). B) Line 1031 uncommented, i.e. with (push) C) Lines 3 & 1033 uncommented, i.e. with (get-unsat-core) D) Same as B) with combined_solver.solver2_timeout=5000 (millisec) E) Same as C) with combined_solver.solver2_timeout=5000 (millisec) F) Same as E) but with if on lines 219-221 in file solver/combined_solver.cpp changed to if (m_ignore_solver1) { (i.e. forcing usage of non-incremental solver1)

Time corresponding to a configuration were as follows: A -> 0.03 sec B -> 151.32 sec C -> 195.48 sec D -> 5.07 sec E -> 194.78 sec F -> 54.18 sec

It seems to me that currently solver2_timeout does not have any influence when parameter produce-unsat-cores is true. Using non-incremental solver queries do seem to be beneficial (or more precisely, preprocessings deployed in non-incremental solver). It might be useful to have a fallback mechanism to a non-incremental solver when querying unsat cores. This may also be related to issue 501.

Does the above make sense to try further exploration? I believe that getting an unsat-core should not take time more than time(config A) * N (N = assumptions.size()), since a MUS can be obtained in this time by using N non-incremental queries using a regular deletion based algorithm (reference).

Attachment: query_bv.smt2.txt

Note - Printing get_num_assumptions() for this query gives 24 (12 + 12)

[anchit]

Have a look at the related issue https://github.com/Z3Prover/z3/issues/1143. Like in this case it is a QF_BV instance but with uninterpreted functions and surprisingly the opposite effect is observed, the incremental solver being faster.

[NikolajBjorner]

The benchmark uses the QF_UF logic. Without incremental mode, auto-configuration used to set different parameters than with incremental mode. This is now changed so that the same mode is used. If you add (set-logic QF_UF) explicitly you will have Z3 use the configuration options relevant for QF_UF also in incremental mode.

Indeed, the running time fluctuates depending on the value of smt.random_seed=.

[NikolajBjorner]

I believe the updates address what we can do from Z3 to make the incremental experience on par with non-incremental even though it requires you to annotate the benchmark with a suitable logic to force the best possible settings