约束非线性优化，值应为0.125的倍数

Question

我正在尝试求解给定输入频率（FIN）和所需输出频率（FOUT）的参数M，D和O。 FOUT = (FIN * M)/(D*O)。我还必须最大化FVCO。 FVCO = (FIN * M)/D。

M和O必须是0.125的倍数，D必须是整数。

我一直在尝试使用scipy.optimize.minimize来完成此操作，但努力寻找办法将M和O的值限制为0.125的倍数，并将D限制为整数。

是否有可以用来完成此任务的库，或者我必须实现自己的算法？

到目前为止我尝试过的：

FIN = 100.0
FOUT = 4.69
MMCM_FIN_MAX = 800.0
MMCM_FIN_MIN = 10.0
MMCM_FOUT_MAX = 800.0
MMCM_FOUT_MIN = 4.69
MMCM_FVCO_MIN = 600.0
MMCM_FVCO_MAX = 1200.0
MMCM_FPFD_MAX = 450.0
MMCM_FPFD_MIN = 10.0
D_MIN = int(math.ceil(FIN/MMCM_FPFD_MAX))
D_MAX = int(math.floor(FIN/MMCM_FPFD_MIN))
M_MIN = math.ceil((MMCM_FVCO_MIN/FIN)*D_MIN)
M_MAX = math.floor((MMCM_FVCO_MAX/FIN)*D_MAX)
O_MIN = 1.0
O_MAX = 128.0

def objective(x):
    return -FIN*(x[0]/x[1])

def constraint1(x):
    return FIN*(x[0]/(x[1]*x[2])) - FOUT

def constraint2(x):
    return -FIN*(x[0]/x[1]) + MMCM_FVCO_MAX

def constraint3(x):
    return FIN*(x[0]/x[1]) - MMCM_FVCO_MIN

x0 = [1, 1, 1]
b1 = (M_MIN, M_MAX)
b2 = (D_MIN, D_MAX)
b3 = (O_MIN, O_MAX)
bnds = (b1, b2, b3)
con1 = {'type': 'eq', 'fun': constraint1}
con2 = {'type': 'ineq', 'fun': constraint2}
con3 = {'type': 'ineq', 'fun': constraint3}
cons = [con1, con2, con3]
sol = minimize(objective, x0, method='SLSQP', bounds=bnds, constraints=cons, options = {'eps': 0.125})
print(sol)

这似乎为我提供了一个在约束范围内的解决方案，但是它返回的带有M，D和O值的数组不是0.125的倍数或整数值。

Answer 1

也许z3py，SAT/SMT solver对于此问题很有用：

from z3 import *

given_FIN = 200
given_FOUT = 1000

D = Int('D')
M8 = Int('M8')  # 8 times M
O8 = Int('O8')  # 8 times O
FIN = Real('FIN')
FOUT = Real('FOUT')
FVCO = Real('FVCO')

s = Optimize()
s.add(FIN == given_FIN)
s.add(FOUT == given_FOUT)
s.add(D > 0)
s.add(FOUT == (FIN * M8 / 8) / (D * (O8 / 8)))
s.add(FVCO == (FIN * M8 / 8) / D )
s.maximize(FVCO)
res = s.check()
print(res)
if res != sat:
    print("No solution found")
else:
    m = s.model()
    print("Found solution:")
    print("  FIN =", m[FIN])
    print("  FOUT =", m[FOUT].numerator_as_long() / m[FOUT].denominator_as_long())
    print("  D =", m[D])
    print("  M = ", m[M8].as_long() / 8)
    print("  O =", m[O8].as_long() / 8)
    print("  FVCO =", m[FVCO].numerator_as_long() / m[FVCO].denominator_as_long())

输出：

sat
Found solution:
  FIN = 200
  FOUT = 100.0
  D = 1
  M =  0.5
  O = 0.0
  FVCO = 100.0