Constrained non-linear optimization, values should be multiples of 0.125

Question

I'm trying to solve for parameters M, D, and O given an input frequency (FIN) and desired output frequency (FOUT). FOUT = (FIN * M)/(D*O). I also have to maximize FVCO. FVCO = (FIN * M)/D.

M and O have to be a multiple of 0.125 and D has to be a whole number.

I've been trying to use scipy.optimize.minimize to accomplish this but struggling to find away to restrict the values tried for M and O to multiples of 0.125 and restrict D to be an integer.

Is there a library that I can use to accomplish this or will I have to implement my own algorithm?

What I have tried so far:

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)

This seems to give me a solution that are within the constraints but the array it returned with the M, D, and O values tried aren't multiples of 0.125 or integer values.

Answer 1

Maybe z3py, a SAT/SMT solver is useful for this problem:

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())

Output:

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