Very long runtime of optimization on seemingly trivial inputs?

[01-eric]

Hi there,

I wanted to preface this by saying that I am new to z3 and SMT solving in general, and I was brought here by a paper that I read on optimizing floorplanning in chip design using SMT/OMT: https://arxiv.org/ftp/arxiv/papers/1709/1709.07241.pdf. In simple terms, I am trying to minimize the bounding box area which surrounds several rectangular modules, each of which can also be moved around and have their dimensions adjusted. Most notably, the objective function and a few of the constraints involve the multiplication of variables since I want the area given by length x width, so the model is not entirely linear. I am aware that non-linear constraints can be a problem for the runtime of optimization algorithms, but the paper also exclusively cites z3 as the tool they used for solving their non-linear model, so I wanted to ask here if there is a way for me to make my model run faster.

I ran a few very simple tests just to gauge the performance of my model and noticed that the solver took very long even on seemingly trivial inputs. For example, I tested the following code, which should very obviously just return the top right corner of the box (8000, 10000):

m = Optimize()
m.add(c <= 8000, d <= 10000, c >= 0, d >= 0)
m.maximize(c * d)
if m.check() == sat:
    print(m.model())
else:
    print("unsat")
print(m.statistics())

but after 30 minutes the solver still had not returned anything and I terminated it. I also changed the reals to ints to see if it would reduce the search time, which it did, but still took upwards of 3 minutes to solve. For such a trivial case this wasn't promising, since eventually I wanted to run this solver with many different blocks, and it wouldn't be scalable with this kind of performance.

In conclusion, I just wanted to ask to see if there is a way I'm missing to make a model involving optimizing area by multiplying variables together faster, preferably with reals. I'm aware that non-linear models are problematic, but since the authors of the paper I linked cited using z3 to solve this problem, I was wondering if you guys could help me out with it. Thanks in advance for any advice!