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:

1. 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)?
2. 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)
&& (u0 >= -2) && (u1 >= -2) && (u0 <= 2) && (u1 <= 2)], Reals]


I, again, quickly get an answer that is "too complicated" - it contains 11 disjunctive bits, when I know that the actual answer must have 5. Running Reduce on the output of the Resolve command above results in a horrendous formula.

Is there an another way to simplify the output of Resolve or force the Resolve command to give an appropriate (i.e. without unnecessary disjunctive bits) answer in the first place? Or is it the case that it depends on the problem, and in some cases, I should not expect to get the answer in the form that I expect?

• Welcome to Mathematica.SE! I suggest the following: 1) As you receive help, try to give it too, by answering questions in your area of expertise. 2) Take the tour! 3) When you see good questions and answers, vote them up by clicking the gray triangles, because the credibility of the system is based on the reputation gained by users sharing their knowledge. Also, please remember to accept the answer, if any, that solves your problem, by clicking the checkmark sign! Commented Feb 24, 2016 at 22:41
• You were close. Run Reduce on the result of Resolve rather than the input. Commented Feb 25, 2016 at 1:54
• Running Reduce on the output of Resolve did the trick. Will have to check if this works for my other problems. I still have a question: why does this redundant disjunctive bit situation happen in the first place? As far as I am aware, Resolve most likely uses cylindrical algebraic decomposition algorithm for quantifier elimination, which should produce disjoint cells where all the polynomial inequalities have the same sign. Am I wrong about this (i.e. another algorithm is used) and is there a way to make Mathematica to produce a proper answer without resulting to tricks like running Reduce? Commented Feb 27, 2016 at 17:58
• Reduce produces a solved formula which is not necessarily simple. There is no built-in command that would eliminate redundant terms of a disjunction. You could use Resolve or FindInstance to test whether a given term of a disjunction is implied by the remaining ones, and iterate this until you get a non-redundant disjunction, but this may be a rather high-cost computation... Commented Mar 3, 2016 at 19:35

Resolve does not use the cylindrical algebraic decomposition (CAD) algorithm here. It uses Weispfenning's quantifier elimination by virtual substitution algorithm to eliminate quantifers and, since its goal is only eliminating quantifiers, it does not solve the resulting quantifier-free inequalities. Reduce needs to produce a solved result and its automatic method choice decides to use CAD from the start. Setting Method->{"QuadraticQE"->True} in Reduce tells it to use virtual substitution to eliminate quantifiers (whenever possible; the method applies to formulas that are at most quadratic in the quantifier variable) and then use CAD to solve the resulting system. For more details search for QuadraticQE in Real Polynomial Systems tutorial.

Reduce[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)], {x0, z}, Reals,