use*_*051 4 smt z3 z3py
任何人都可以告诉我如何通过Z3py实现最小化整数问题,如下所示？我如何定义所有声明？这里所有变量都是int sort.
Z3中是否有专门的求解器可以解决这类问题？如果有,那么我该如何设置该求解器的配置？
谢谢
Leo*_*ura 7
以下是一些相关/类似的问题和答案:
变量的最小值和最大值
确定任意命题公式中变量的上限/下限
如何在Z3中优化一段代码？(PI_NON_NESTED_ARITH_WEIGHT相关)
Z3是否支持优化问题
归档时间：
12 年，3 月 前
查看次数：
1033 次
最近记录：
