Hi there,
I have a big system of inequalities (~1500 inequalities, 45 variables) and want to check, if there exists a real solution to it. Trying out the 'solve' and 'solve_ineq' takes a huge amount of time or it breaks during calculation and after checking some of the questions here I even assume the solve-function is broken and sometimes gives wrong results. Does anybody know about a function/system which returns in a responsible time and reliable if there exists a solution or not (existence is enough) (I want to use this in an actual proof, so it would be useless, if I can't trust the result).
In my use case I have the variables $a1, ..., a15, b1,...,b15,c1,...,c15 \in \mathbb R^+$ and my inequalities are all of the form $$ \frac{f(a1,...,a15)}{g(c1,\dots, c15)} \geq \frac{f'(a1,\dots,a15)}{g'(c1,\dots, c15)}$$ (and same for combinations of (a,b) and (b,c)) for given linear functions $f,f',g,g'$ (i.e. multivariate polynomials with degree at most 1), so restricting to the variables $ai$ we get a system of linear inequalities (but even trying to solve these takes long/doesn't work with the solve function).
Actually more accuratly I have indexed sets $$F_{a,b} ={{(f_i,g_i) | i \in I }, F_{c,b} ={(p_i,q_i) | i \in I } ,F_{a,c} ={(r_i,s_i) | i \in I } $$ and want to show, that if there exists a solution $(a,b)$ of $$\frac{f_k(a)}{g_k(b)} = max_i \frac{f_i(a)}{g_i(b)}$$ then there exists a solution $(c)$ to $$\frac{r_k(a)}{s_k(c)} = max_i \frac{r_i(a)}{s_i(c)}\ \frac{p_k(c)}{q_k(b)} = max_i \frac{p_i(c)}{q_i(b)} $$
So far I have a the follwing snippet:
#fractionAB are the saved fractions from above, a,b,c are arrays with e.g. a=[a1,a2,...,a15]
stopIt=False
for maxStretch in cands: #cands is the index set I
ineq=[fractionAB.get(maxStretch) >= fractionAB.get(cand) for cand in cands]
if solve(ineq,a+b)
#try here if there exists a middle point on the geodesic, i.e. geodesic exists
ineq.expand([fractionAC.get(maxStretch) >= fractionAC.get(cand) for cand in cands])
ineq.expand([fractionCB.get(maxStretch) >= fractionCB.get(cand) for cand in cands])
if not solve(ineq, a+b+c):
stopIt=True
print 'Tested for candidate ' , maxStretch
if stopIt:
break
I know, there is room for improvement e.g. at reusing to first solution from (a+b), the problem is, that even that first system pretty much kills the calculation.
PS: The mathjax seems to be broken on this site, since the code for leftbraces seems to vanish (hence the ugly "fix" above).