CODEWITHSUNDEEP
z3z3py
user4233211
user4233211

Reputation:

Will Z3 adaptively change strategy in solving linear real arithmetic constraints?

I have a huge set of linear real arithmetic constraints to solve, and I am incrementally feeding them to the solver. Z3 always seems to get stuck after a while. Is Z3 internally going to change its strategy in solving the constraints, such as moving away from the Simplex algorithm and try others, etc. Or do I have to explicitly instruct Z3 to do so? I am using Z3py.

Upvotes: 0

Views: 91

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8402

Without further details it's impossible to answer this question precisely.

Generally, with no logic being set and the default tactic being run or (check-sat) being called without further options, Z3 will switch to a different solver the first time it sees a push command; prior to that it can use a non-incremental solver.

The incremental solver comes with all the positives and negatives of incremental solvers, i.e., it may be faster initially, but it may not be able to exploit previously learned lemmas after some time, and it may simply remember too many irrelevant facts. Also, the heuristics may 'remember' information that doesn't apply at a later time, e.g., a 'good' variable ordering may change into a bad one after everything is popped and a different problem over the same variables is pushed. In the past, some users found it works better for them to use the incremental solver for some number of queries, but to start from scratch when it becomes too slow.

Upvotes: 2

Related Questions