Efficiently computing Gröbner basis to prove no solution to polynomial constraints In a similar vein to these now quite old questions on advice for calculating a Gröbner basis:
Fast computation of a Groebner basis. What is possible?
What is the state of art in Groebner bases
I am interested in advice/tips/tricks for computing a Gröbner basis, but in the case where we likely already know the answer is {1}. In this case the computation is used to verify there are no solutions to a large set of multivariate polynomial constraints.
Macaulay2 seems to systematically build up larger and larger degrees of polynomials, while Mathematica (which is usually slower and is opaque in its computations) can sometimes run dramatically faster than Macaulay2 for this use case (possibly Mathematica does a more "depth first" search which can lead to contradictions quicker?). I've seen cases where Mathematica takes ~ 4 min, while Macaulay takes > 20 hours.
In particular, the RAM requirements for these runs is often the limited factor, when all I really want to know is the "ideal membership problem" for 1. So I wonder if:

Is there a more appropriate calculation, computational package, or algorithm for calculating the Gröbner basis with the "hint" that there is very likely some relationship that collapses everything to {1}?

 A: When I personally have implemented these ideas: I use Groebner basis as the "last resort". Try the "linear algebra" trick -- Suppose you have $p_1 = 0 \land p_2 = 0 \land \cdots p_n = 0$, you want to find if there exist $g_1, \ldots, g_n$ such that $ \sum_{i=1}^n g_i p_i = 1$. I fix the degree of $g_i$ to a bound (say 2) and generate all possible monomials of that degree. Then we can generate a system of linear equations on these unknowns by comparing LHS coefficients with those in the RHS to check if there is a solution. This is often way faster for some systems and may be able to resolve your question. However, there are no guarantees. In fact, there is a theorem that puts an upper bound on the degrees of the polynomials $g_i$ you need to search on, but that bound is double exponential in the number of variables, and n if I am not mistaken (look for effective nullstellensatz: https://encyclopediaofmath.org/wiki/Effective_Nullstellensatz ). If not, you will have no choice but use either Wu-Ritt method (but be careful since you may be missing some solutions) or Groebner basis (which will give you the precise answer). I do not always have access to Mathematica but there are many "free" options that would included Singular, Macaulay, Sage, GROBNER library, sympy in Python,... I usually give them a try and see if they can solve the problem. Mathematica has dedicated programmers who likely spend a lot of time engineering these tools whereas other tools are open source and written by academics. Hope this helps answer your question.
