I'm writing a program that scrapes option_chain data off the TMX website and suggests an optimized Covered Call options portfolio based on those data. for the optimization process, I used the z3py library as discussed on this website by many users. the optimization process works by maximizing the premiums and setting the portfolio delta to a user-specified amount.
initially, I made a mistake in my calculation for portfolio delta which made everything work so smoothly but I'm facing issues after correcting it. portfolio delta is calculated by taking the Weighted average delta of non-zero positions in the portfolio. to achieve this I used the following setup:
eng = Optimize()
Weights = [Real(row.symbol) for row in df.itertuples()]
#to count non-zero positions
TotCount = Real("TotCount")
eng.add(TotCount == Sum([If(w > 0, 1, 0) for w in Weights]))
eng.add(TotCount == If(TotCount >= 0, TotCount, 1))
#to get portfolio delta
eng.add(TotDelta == (Sum([(w * row.delta) for w, row in zip(Weights, df.itertuples())]) / TotCount))
eng.add(TotDelta == delta)
res = eng.check()
the weird behavior happens when I run this as a function in a loop with different values for delta, the first loop actually does the calculation and spits out an answer but after that my code gets stuck on the last line for hours without any progress. i tried a few things like completely reformatting it but nothing seems to make a difference. I was wondering if anyone knows what's happening here or not?
Unfortunately, there isn't much in your description for anyone to go on without knowing further details of your setup. All one can deduce from your text is that the constraints are hard to solve for those values of delta where it takes longer. Without seeing the rest of your program, it's impossible to opine on what else might be going on.
See if you can isolate the value of delta that it runs slowly on, and just run it for that one instance separately to see if there's interaction coming from elsewhere. That's by no means a solution of course, but it's one way to get started.
One thing I noticed, though, is this line you have:
eng.add(TotCount == If(TotCount >= 0, TotCount, 1))
Let's see what this line is saying: If TotCount >= 0, then it says TotCount == TotCount. i.e., it puts no restrictions on it. Otherwise, it says TotCount == 1; i.e., if TotCount < 0, then TotCount == 1. Well this latter statement is obviously false. That is if, the other constraints force TotCount < 0, then your program would be unsat. This essentially means that whole line is functionally equivalent to:
eng.add(TotCount >= 0)
It's hard for anyone to tell if that's what you intended; but I suspect perhaps it isn't; since you'd have just written the simpler form above. Perhaps you wanted to say something more along the lines of if TotCount < 0, then make it 1. But looking at the previous line, (i.e., the Sum expression), we see that this'll never be the case. So, something is fishy there.
Hope that helps to get you started; note that you cannot model "sequential assignment" like in a programming language in this way. (You'd need to do what's known as single static assignment, a.k.a. SSA, conversion.) But then again, without knowing your exact intention, it's hard to opine.