# Quantifier elimination by using Resolve outputs a formula that is “too complicated”

The following command:

Resolve[Exists[{u0, u1, u2},
(z >= u0^2 + u1^2 + u2^2 + 100*((7 u2)/20 +
13/20 ((2 u1)/5 + 3/5 ((9 u0)/20 + (11 x0)/20)) – 1500)^2)
&& ((55/100)*x0 + (45/100)*u0 >= 200)
&& ((55/100)*x0 + (45/100)*u0 <= 400) && ((2 u1)/5 + 3/5 ((9 u0)/20 + (11 x0)/20) >= 500)
&& ((2 u1)/5 + 3/5 ((9 u0)/20 + (11 x0)/20) <= 1000) && (u0 >= 0) && (u1 >= 0) && (u2 >= 0) && (u0 <= 3000) && (u1 <= 3000) && (u2 <= 3000)], Reals] // Timing gives the output of the form: {0.175804, (x0 <= 4000/11 && x0 >= -(23000/11) && -88000 x0 + 121 x0^2 – 81 z <= -944665000) || (x0 <= 4000/11 && x0 >= -(23000/11) && -88000 x0 + 121 x0^2 – 81 z <= -(45035120000/53)) || (x0 <= 4000/11 && x0 >= -(23000/11) && -88000 x0 + 121 x0^2 – 81 z <= -(556634680000/667)) || (x0 <= -(19000/11) && x0 >= -(23000/11) && 2046000 x0 + 1089 x0^2 -1600 z <= -32261000000) || (x0 <= -(19000/11) && x0 >= -(23000/11) && -1254000 x0 + 1089 x0^2 – 1600 z <= -(1244733000000/53) && z > 0) ||
(x0 <= -(19000/11) && x0 >= -(23000/11) && -3105762000 x0 + 5230467 x0^2 – 6624800 z <= -98750283000000 && z > 0) ||
(x0 <= -(19000/11) && x0 >= -(23000/11) && 131274000 x0 + 184041 x0^2 – 310400 z <= -5610609000000) || (x0 <= -(19000/11) && x0 >= -(23000/11) && -556842000 x0 + 61347 x0^2 – 266800 z <= -3664803000000 && z > 0) ||
(x0 <= 8000/11 && x0 >= -(19000/11) && -176000 x0 + 121 x0^2 – 81 z <= -953785000) || (x0 <= 8000/11 && x0 >= -(19000/11) && -176000 x0 + 121 x0^2 – 81 z <= -(42298730000/53)) || (x0 <= 8000/11 && x0 >= -(19000/11) && -176000 x0 + 121 x0^2 – 81 z <= -(530398720000/667)) || (x0 <= 8000/11 && x0 >= 4000/11 && -3300000 x0 + 1089 x0^2 – 1600 z <= -19400000000) || (x0 <= 8000/11 && x0 >= 4000/11 && -6600000 x0 + 1089 x0^2 – 1600 z <= -(992400000000/53)) || (x0 <= 8000/11 && x0 >= 4000/11 && -59400000 x0 + 14157 x0^2 – 20800 z <= -(3243600000000/13)) || (x0 <= 8000/11 && x0 >= 4000/11 && -28782600000 x0 + 5230467 x0^2 – 6624800 z <= -78262800000000) || (x0 <= 8000/11 && x0 >= 4000/11 && -772200000 x0 + 184041 x0^2 – 310400 z <= -3603600000000) || (x0 <= 8000/11 && x0 >= 4000/11 && -858000000 x0 + 61347 x0^2 – 266800 z <= -3000000000000) || (x0 <= 16205/44 && x0 >= -(7085/44) && -3300000 x0 + 1089 x0^2 – 2329 z <= -27100062500) || (x0 <= -(7085/22) && x0 >= -(9365/11) && -6600000 x0 + 1089 x0^2 – 2329 z <= -(1203081000000/53) && z > 0) ||
(x0 <= -(46975/44) && x0 >= -(5725/4) && 1218525 x0 + 2178 x0^2 – 3200 z <= -(394964455625/8)) || (x0 <= -(19000/11) && x0 >= -(23000/11) && -1254000 x0 + 1089 x0^2 – 1600 z <= -(348509729000000/13689) && z > 0) ||
(x0 <= -(19000/11) && x0 >= -(23000/11) && 2046000 x0 + 1089 x0^2 – 1600 z <= -(22271800121000000/670761)) || (x0 <= 8000/11 && x0 >= 4000/11 && -6600000 x0 + 1089 x0^2 – 1600 z <= -(952400000000/49)) || (x0 <= 782135/4268 && x0 >= -(692935/2134) && -772200000 x0 + 184041 x0^2 – 433601 z <= -4712409000000) || (x0 <= 4000/11 && x0 >= -(5725/4) && -1222462472000 x0 + 3458297249 x0^2 – 1686498489 z <= -18618154759760000) || (x0 <= 8000/11 && x0 >= -(46975/44) && -4008629944000 x0 + 3458297249 x0^2 – 1686498489 z <= -18421094448290000) || (x0 <= 8000/11 && x0 >= 4000/11 && -6600000 x0 + 1089 x0^2 – 1600 z <= -(952400000000/49)) || (x0 <= -(19000/11) && x0 >= -(23000/11) && -1254000 x0 + 1089 x0^2 – 1600 z <= -(348509729000000/13689) && z > 0) ||
(x0 <= -(19000/11) && x0 >= -(23000/11) && 2046000 x0 + 1089 x0^2 – 1600 z <= -(22271800121000000/670761)) || (x0 <= -(5725/4) && x0 >= -(23000/11) && -64521512000 x0 + 986978729 x0^2 – 488984769 z <= -5845319470272500 && z > 0) ||
(x0 <= 4000/11 && x0 >= -(23000/11) && -245216312000 x0 + 986978729 x0^2 – 488984769 z <= -5209358474960000) || (x0 <= -(46975/44) && x0 >= -(19000/11) && -782324224000 x0 + 986978729 x0^2 – 488984769 z <= -5764578733152500 && z > 0) ||
(x0 <= 8000/11 && x0 >= -(19000/11) && -963019024000 x0 + 986978729 x0^2 – 488984769 z <= -4827586361090000) || (x0 <= 4000/11 && x0 >= -(23000/11) && -245216312000 x0 + 986978729 x0^2 – 488984769 z <= -5209358474960000) || (x0 <= -(5725/4) && x0 >= -(23000/11) && -64521512000 x0 + 986978729 x0^2 – 488984769 z <= -5845319470272500 && z > 0) ||
(x0 <= 8000/11 && x0 >= -(19000/11) && -963019024000 x0 + 986978729 x0^2 – 488984769 z <= -4827586361090000) || (x0 <= -(46975/44) && x0 >= -(19000/11) && -782324224000 x0 + 986978729 x0^2 – 488984769 z <= -5764578733152500 && z > 0) ||
(x0 <= 4000/11 && x0 >= -(23000/11) && -2629445896000 x0 + 12674552407 x0^2 – 6323537727 z <= -66543336410680000) || (x0 <= 8000/11 && x0 >= -(19000/11) && -12208691792000 x0 + 12674552407 x0^2 – 6323537727 z <= -62261601502720000) || (x0 <= 8000/11 && x0 >= 4000/11 && -2574000000 x0 + 184041 x0^2 -760400 z <= -9000000000000) || (x0 <= -(51813475165/179450678) && x0 >= -(69536290885/89725339) && -4507447800000 x0 + 807528051 x0^2 – 1586529211 z <= -(170100022281000000/11) && z > 0) ||
(x0 <= -(692935/2134) && x0 >= -(9365/11) && 1139192148160 x0 + 1245544355 x0^2 – 162994923 z <= -2111574155307200) || (x0 <= -(7085/22) && x0 >= -(9365/11) && -127694245800000 x0 + 23311622961 x0^2 – 44918139721 z <= -437813124681000000 && z > 0) ||
(x0 <= 782135/4268 && x0 >= -(7085/22) && 121166376320 x0 + 1245544355 x0^2 – 162994923 z <= -1656536615628800) || (x0 <= -(19000/11) && x0 >= -(23000/11) && -4131578000 x0 + 552123 x0^2 – 2281200 z <= -(53122168267000000/1521) && z > 0) ||
(x0 <= -(1740160/7337) && x0 >= -(4818830/7337) && -858000000 x0 + 61347 x0^2 – 307867 z <= -3000000000000 && z > 0)}

As you can see, there are a lot of unnecessary disjunctive bits in this formula – for example, Simplify command on the first three disjunctive bits:

Simplify[
(x0 <= 4000/11 && x0 >= -(23000/11)
&& -88000 x0 + 121 x0^2 – 81 z <= -944665000) || (x0 <= 4000/11 && x0 >= -(23000/11)
&& -88000 x0 + 121 x0^2 – 81 z <= -(45035120000/53)) || (x0 <= 4000/11 && x0 >= -(23000/11)
&& -88000 x0 + 121 x0^2 – 81 z <= -(556634680000/667))] returns the third disjunctive bit x0 >= -(23000/11) && 11 x0 <= 4000 && 556634680000/667 + 121 x0^2 <= 88000 x0 + 81 z since it obviously implies the other two. Also, I know that the actual answer (which I obtained in two ways: by splitting the original Resolve problem into 3 smaller ones, and by using a multi-parametric optimisation approach (that is not dependant on quantifier elimination) in Matlab) consists of only three disjunctive bits: {(-(23000/11) <= x0 <= -(4818830/7337) && z >= (556634680000 – 58696000 x0 + 80707 x0^2)/54027) ||
(-(4818830/7337) < x0 <= -(1740160/7337) && z >= (3000000000000 – 858000000 x0 + 61347 x0^2)/307867) ||
(-(1740160/7337) < x0 <= 8000/11 && z >= (530398720000 – 117392000 x0 + 80707 x0^2)/54027)}

Also, please notice that the second disjunctive bit of this actual answer is the same as the last disjunctive bit in the horrible output provided by Mathematica. Hence, I have a suspicion that these two formulas are equivalent (as you would expect), but I was unsuccessful at trying to reduce the original Mathematica answer to the one I expected to get.

Hence, my questions are:

Are there ways to force Resolve to give me the solution I expect (or at least a solution that is simpler and does not contain superfluous disjunctive bits)?
Is there a way to check equivalence of two logical formulas involving real arithmetic (Equivalent seems to work only on Boolean expressions)?

Also, please note that using Reduce on the original problem and asking it to express the output in terms of z does not terminate in 24 hours.

Ok, when I run the following command which is similar in its structure to the original one:

Resolve[Exists[{u0, u1},
(z >= (981*u0*u1)/1250 + (6562926851980997*u0*x1)/562949953421312
+ (4677*u0*x2)/400 + (52771*u1*x1)/5000 + (6614*u1*x2)/625 +
(1519*u0^2)/2500 + (1519*u1^2)/2500)