I'm trying to solve an SMT problem containing linear integer modulo theory with Z3 (Python). The problem is similar to the "Learning a Boolean Function" example on pp. 14f of Knuth's satisfiability book. My problem has a set of Boolean-valued formulas (hundreds), each containing the same set of unknown integer and Boolean variables to be solved for (tens), and the optimization objective is to maximize the number of true formulas as a function of these unknowns. I'm trying to improve the solution speed. The formulas contain mixed Boolean variables with expressions like (x <= const) or (x1 + x2 <= const) or (x == x1 + x2) for integers x, x1, x2, const.
From experiments I've learned: (1) using bisection on the decision problem (repeatedly solve for objective function >= a given constant) using z3.Solver() seems much faster than using z3.Optimize() directly; (2) using the tactic "dt2bv" seems to greatly improve speed. However, it still takes hours or days of runtime to solve a single large problem.
It looks like Z3 has over 100 tactics with over 9000 total options, though much of these seem to be allocated to very specialized problem types. Any assistance on where to look for making this run much faster would be much appreciated. I'd be happy to post diagnostic output from a sample run if it is helpful. Thanks in advance for your reply.
There's no one-size-fits all "recommendation," I'm afraid. You can search stack-overflow for many questions asking for how to improve speed of z3, and the answer is always "extremely problem specific" if at all possible.
What you are doing, i.e., experimenting with different ideas/options is the right way to go. Note that while z3 has a ton of tactics, most won't apply. Unfortunately these tactics are very poorly documented, if at all.
Also, it isn't surprising that you're finding your own "binary-search" like implementation performs better than the optimizer itself. Unfortunately the optimizer implementation in z3 has not received much attention, in particular it is not incremental. So, if you find implementing your own search performs better, definitely go with that. Alternatively, you can look at OptiMathSat. It uses a different style of optimization, and might perform better on this particular problem. (I'm not claiming it will; All I'm saying is it's worth a try.)