How can I solve minimizing constraint in Z3?

问题:

Could any one can tell me how I can implement minimizing integer problem like the below one by Z3py? How can I define for all statement? Here all variables are int sort.

Is there any dedicated solver within Z3 is available to solve such kind of problem? If there any, then how can I set configuration for that solver?

Thanks

回答1:

Here are some relevant/similar questions and answers:

• Minimum and maximum value of variable

• Determine upper/lower bound for variables in an arbitrary propositional formula

• How to optimize a piece of code in Z3? (PI_NON_NESTED_ARITH_WEIGHT related)

• Does Z3 have support for optimization problems