How to use incremental solving with z3py

Question

I am using the python API of the Z3 solver to search for optimized schedules. It works pretty well apart from that it sometimes is very slow even for small graphs (sometimes its very quick though). The reason for that is probably that the constraints of my scheduling problem are quite complex. I am trying to speed things up and stumbled on some articles about incremental solving. As far I understood, you can use incremental solving to prune some of the search space by only applying parts of the constraints.

So my original code was looking like that:

for constraint in constraint_set:
    self._opt_solver.add(constraint)
self._opt_solver.minimize(some_objective)
self._opt_solver.check()
model = self._opt_solver.mode()

I changed it now to the following:

for constraint in constraint_set:
    self._opt_solver.push(constraint)
    self._opt_solver.check()
self._opt_solver.minimize(some_objective)
self._opt_solver.check()
model = self._opt_solver.mode()

I basically substituted the "add" command by the "push" command and added a check() after each push.

So first of all: is my general approach correct? Furthermore, I get an exception which I can't get rid of:

self._opt_solver.push(constraint) TypeError: push() takes 1 positional argument but 2 were given

Can anyone give me a hint, what I am doing wrong. Also is there maybe a z3py tutorial that explains (with some examples maybe) how to use incremental solving with the python api.

My last question is: Is that at all the right way of minimizing the execution time of the solver or is there a different/better way?

alias alias · Accepted Answer · 2018-07-10T19:14:21

The function push doesn't take an argument. It creates a "backtracking" point that you can pop to later on. See here: http://z3prover.github.io/api/html/classz3py_1_1_solver.html#abc4ae989afee7ad164844640537107d9

So, it seems push isn't really what you want/need here at all. You should simply add your constraints one-by-one and call check. However, I very much doubt checking after each addition is going to speed anything up significantly. The optimizing solver (as opposed to the regular one), in particular, usually solves everything from scratch. (See the relevant discussion here: https://github.com/Z3Prover/z3/issues/1577)

Regarding incremental: The python API is automatically "incremental." Incremental simply means the ability to call the command check() multiple times, without the solver forgetting what it has seen before. (i.e., call check, assert more facts, call check again; the second check will take into account all the assertions from the very beginning.) You shouldn't make any assumptions regarding this will give you speed over calling check just once at the very end: It entirely depends on the heuristics and the decision procedures involved, which is dependent on the problem at hand.

How to use incremental solving with z3py

1 Answers