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.