Solving a high number of equalities/inequalities

Question

i got stuck on the following problem. Let $f_1,...,f_r \in \mathbb{R}[x_1,...,x_n]$ be some polynomials. The question is if there is any real value $x$ such that $f_1,..,f_i$ are zero in $x$ and $f_{i+1},...,f_r$ are non-zero.

The problem is that I have given about 200 such polynomials in about 200 variables. I can reformulate the problem so one can theoretically solve it using Gröbner basis and such, but there is no point in calculating that in any reasonable time.

Does anyone know a program to do this? I especially never used the fact that i just want to know if there is a solution and I dont need every such solution. Is there any chance using maple?

Thanks in advance

Answer 1

You may want to try Z3. Here's a simple example that uses the python API. I've no idea how Z3 will fare on your problem, but at least in principle it can handle it.

from __future__ import print_function
from z3 import *

x0, x1 = RealVector('x', 2)

poly = [
    x0**3 - 2*x1**2 + 4*x1,
    -x1**2 + 5*x0 + 7,
    x0**2 - x1,
    x1**2 + x0**2 - 3*x1
]

constraints = [
    poly[0] == 0,
    poly[1] == 0,
    poly[2] != 0,
    poly[3] != 0
]

s = Solver()
s.add(constraints)
if s.check() == sat:
    mdl = s.model()
    print(mdl)
    print([mdl.evaluate(p) for p in poly])
else:
    print('unable to solve')