incremental solving with nlsat solver

Question

I'm attempting to implement the quick-explain algorithm with the 'nlsat' solver. As the algorithm requires to solve a subset of the original constraint set many times, I decide to use the push/pop function in z3 c++ interface.(check(assumptions) does not work in nlsat solver). A selector variable is used to imply adding/removing a constraint.

But I experienced a problem when solving a constraint set. z3 is able to tell me the whole constraint set is unsat in less than 1 minute. But when checking a subset of the original constraint set, it didn't give a result for more than 1 hour.

The whole constraint set can be solved in less than 1 minute

a subset of the original constraint set can't get a result for more than 1 hour

What changes the performance dramatically? In general, what affects the performance of nlsat solver?

Any suggestion is appreciated.

Answer 1

The nlsat solver does not expose incrementality, so when you create multiple queries it will start from scratch. For your shorter formulas it may be the case that the search space is much bigger.