Maximizing quantities/length in buckets to match each other

I have a use case, real one, and I'm trying to come up with an efficient maximization algorithm to solve it.

I'll try to simplify, with a simple analogue, and after will explain the real world use case:

Analogue:

Imagine you have 2 buckets of springs.
Each spring has 2 properties: resting length, and maximum stretching length.
Some springs are basically just rods, and resting length = maximum stretch length.

Your job is to maximize length of joined springs (& rods) in each bucket, such that the length of the 2 joined springs in the 2 buckets match exactly.

Example:

A bucket of springs $S_k$ is a non-empty multiset of intervals $[i,j]$, where $i$ denotes the "resting length", and $j$ denotes the "maximal stretch length". For example, if the two buckets are

$$\begin{align*}
S_1&=\{[2,4],[2,4],[4,4]\} \\
S_2&=\{[1,1],[2,4],[13,15]\}
\end{align*}$$
then the maximum achievable length is 5, since $2 + 3 = 1 + 4$ and $2 \in [2,4]$ and $3 \in [2,4]$ and $1 \in [1,1]$ and $4 \in [2,4]$.

Note that if the last spring in $S_2$ would have been $[12,15]$ instead of $[13,15]$, the maximum length would have been $12$ (by the choice $4+4+4=12$). But since lengths in each bucket must match exactly, we end up with only $5$.

Real (boring) problem:

My use case is from the finance world. I'm trying to match buy orders & sell orders for different amounts. Some of the orders can be partially accepted, whilst other must be strictly accepted or rejected. The orders I can partially accept, also specify the minimum amount it must be accepted with.

Each order is a "spring" in the analogy, where "resting length" is minimum accepting amount, and "maximum stretching length" is the full amount. The 2 buckets are the buy orders & sell orders.

Also, note that for now I've been asked to maximize amounts, but a further complication of the algorithm would be to maximize both amount & price. Either by preferring amount over price, and when there's a choice, to prefer the better price (low

I would solve this problem with an SMT solver like z3. Example in Python:

`import z3

buckets = [
[(2, 4), (2, 4), (4, 4)],
[(1, 1), (2, 4), (13, 15)],
]

solver = z3.Optimize()

m = z3.Int("m")

for bnr, bucket in enumerate(buckets):
springs = []
for b, (lo, hi) in enumerate(bucket):
include_spring = z3.Bool(f"is{bnr},{b}")
spring = z3.Real(f"s{bnr},{b}")
solver.add(lo

The constraints are easy to express and SMT solvers are really quite powerful nowadays.

StackExchange Computer Science Q#97111, answer score: 2