约束非线性优化，值应为 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