Positive Solutions of Systems of Signed Parametric Polynomial Inequalities

• Hoon Hong
• Thomas Sturm
Open Access
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11077)

Abstract

We consider systems of strict multivariate polynomial inequalities over the reals. All polynomial coefficients are parameters ranging over the reals, where for each coefficient we prescribe its sign. We are interested in the existence of positive real solutions of our system for all choices of coefficients subject to our sign conditions. We give a decision procedure for the existence of such solutions. In the positive case our procedure yields a parametric positive solution as a rational function in the coefficients. Our framework allows to reformulate heuristic subtropical approaches for non-parametric systems of polynomial inequalities that have been recently used in qualitative biological network analysis and, independently, in satisfiability modulo theory solving. We apply our results to characterize the incompleteness of those methods.

1 Introduction

We investigate the problem of finding a parametric positive solution of a system of signed parametric polynomial inequalities, if exists. We illustrate the problem by means of two toy examples:
$$f(x) = c_2x^2-c_1x+c_0,\quad g(x) = -c_2x^2+c_1x-c_0,$$
where $$c_2$$, $$c_1$$, $$c_0$$ are parameters. An expression $$z(c)$$ is called a parametric positive solution of $$f(x)>0$$ if for all $$c>0$$ we have $$z(c)>0$$ and $$f(z(c))>0$$. One easily verifies that $$z(c)=\frac{c_1}{c_2}$$ is a parametric positive solution of f(x). However, $$g(x)>0$$ does not have any parametric positive solution since $$g(x)>0$$ has no positive solution when, e.g., $$c_2=c_1=c_0=1$$. Of course, we are interested in tackling much larger cases with respect to numbers of variables, monomials, and polynomials.

The problem is important as systems of polynomial inequalities often arise in science and engineering applications, including, e.g., the qualitative analysis of biological or chemical networks [7, 20, 21, 40] or Satisfiability Modulo Theories (SMT) solving [1, 22, 32]. In both these areas, one is indeed often interested in positive solutions. For instance, unknowns in the biological and chemical context of [7, 20, 21, 40] are positive concentrations of species or reaction rates, where the direction of the reaction is known. In SMT solving, positivity is often not required but, in the satisfiable case, benchmarks typically have also positive solutions; comprehensive statistical data for several thousand benchmarks can be found in [22]. In many areas systems have parameters and one desires to have parametric solutions. Hence, an efficient and reliable tool for finding parametric positive solutions can aid scientists and engineers in developing and investigating their mathematical models.

The problem of finding parametric positive solutions is essentially that of quantifier elimination over the first order theory of real closed fields. In 1930, Tarski [38] showed that real quantifier elimination can be carried out algorithmically. Since then, there has been intensive research, producing profound theories with dramatically improved asymptotic complexity, e.g., [5, 10, 14, 24, 33]. Practical complexity was improved as well, often in combination with highly refined implementations, e.g., [2, 8, 11, 13, 17, 23, 25, 26, 27, 28, 30, 35, 36, 41]. Today several implementations of real quantifier elimination are available in well-supported computer algebra software such as Maple [11, 43], Mathematica [42, later editions online], Qepcad B [9], or Reduce [18, 28]. However, existing general quantifier elimination software is still too inefficient for finding parametric positive solutions with relevant problem sizes in our above-mentioned fields of applications.

The main contribution of this paper is to provide simple and practically efficient algorithmic criteria for deciding whether or not a given signed parametric system has a parametric positive solution. To be precise, we reduce the problem to SMT solving over quantifier-free linear real arithmetic (QF_LRA). In case of existence we provide an explicit formula (rational function) for a parametric positive solution. The main challenge was eliminating many universal quantifiers in the problem statement. We tackled that challenge by, firstly, carefully approximating/bounding polynomials by suitable multiple of monomials and, secondly, tropicalizing, i.e., linearizing monomials by taking logarithms in the style of [39]. However, unlike standard tropicalization approaches, we determine sufficiently large finite bases for our logarithms, in order to get an explicit formula for parametric positive solutions.

Our main result also shines a new light on recent heuristic subtropical methods [22, 37]: We provide a precise characterization of their incompleteness in terms of the existence of parametric positive solutions for the originally non-parametric input problems considered there. Furthermore our approach is applicable to generalized polynomials with real exponents. Such polynomials have been studied for related but different questions, also in the context of chemical reaction networks, in [31].

The paper is structured as follows. In Sect. 2, we motivate and present a compact and convenient notation for a system of multivariate polynomials, which will be used throughout the paper. In Sect. 3, we precisely define the key notions of signed parametric systems and parametric positive solutions. Then we present and prove the main result of this paper, which shows how to check the existence of a parametric positive solution and, in the positive case, how to find one. In Sect. 4, we apply our framework and our result to re-analyze and improve the above-mentioned subtropical methods [22, 37].

2 Notation

The principal mathematical object studied in this paper are systems of multivariate polynomials over the real numbers. In order to minimize cumbersome indices, we are going to introduce some compact notations. Let us start with a motivation by means of a simple example. We are going to use hat accents, like $$\hat{f}$$, for naming polynomials and systems with concrete coefficients in contrast to parametric ones, which we will introduce and discuss in the next section.

Example 1

Consider the following system of three polynomials in two variables:
\begin{aligned} \hat{f}_1&=-x_1^5+4x_1^2x_2-2x_1^2+x_2^2\\ \hat{f}_2&=6x_1^5+x_1^2x_2+7x_1^2-3x_2^3\\ \hat{f}_3&=4x_1^5+x_1^2x_2-2x_1^2-5x_2^3. \end{aligned}
We rewrite those polynomials by aligning their signs, coefficients, and monomial support:
$$\begin{array}[b]{llrlllrlrll} \hat{f}_{1} &{}= &{} -1\cdot 1\cdot x_{1}^{5}x_{2}^{0} &{} + &{} 1\cdot 4\cdot {} x_{1}^{2}x_{2}^{1} &{} + &{} -1\cdot 2\cdot {} x_{1}^{3}x_{2}^{0} &{} + &{} 0\cdot 1\cdot {} x_{1}^{2}x_{2}^{0} &{} + &{} 1\cdot 1\cdot {} x_{1}^{0}x_{2}^{2}\\ \hat{f}_{2} &{} = &{} \quad 1\cdot 6\cdot {} x_{1}^{5}x_{2}^{0} &{} + &{} 1\cdot 1\cdot {} x_{1}^{2}x_{2}^{1} &{} + &{} 1\cdot 7\cdot {} x_{1}^{3}x_{2}^{0} &{} + &{} -1\cdot 3\cdot {} x_{1}^{2}x_{2}^{0} &{} + &{} 0\cdot 1\cdot {} x_{1}^{0}x_{2}^{2}\\ \hat{f}_{3} &{} = &{} 1\cdot 4\cdot {} x_{1}^{5}x_{2}^{0} &{} + &{} 1\cdot 1\cdot {} x_{1}^{2}x_{2}^{1} &{} + &{} -1\cdot 2\cdot {} x_{1}^{3}x_{2}^{0} &{} + &{} -1\cdot 5\cdot {} x_{1}^{2}x_{2}^{0} &{} + &{} 0\cdot 1\cdot {} x_{1}^{0}x_{2}^{2}\\ \end{array},$$
where signs are represented by $$-1$$, 0, and 1. Note that we are writing 0 coefficients as $$0\cdot 1$$ for notational uniformity. Rewriting this in matrix-vector notation, we have
$$\begin{bmatrix} \hat{f}_{1}\\ \hat{f}_{2}\\ \hat{f}_{3} \end{bmatrix} =\left( \begin{bmatrix} -1&1&-1&0&1\\ 1&1&1&-1&0\\ 1&1&-1&-1&0 \end{bmatrix} \circ \begin{bmatrix} 1&4&2&1&1\\ 6&1&7&3&1\\ 4&1&2&5&1 \end{bmatrix} \right) \begin{bmatrix} x_1^5x_2^0\\ x_1^2x_2\\ x_1^2x_2^0\\ x_1^0x_2^3\\ x_1^0x_2^2 \end{bmatrix},$$
where $$\circ$$ is the component-wise Hadamard product. Pushing this even further, we finally obtain
$$\begin{bmatrix} \hat{f}_{1}\\ \hat{f}_{2}\\ \hat{f}_{3} \end{bmatrix} =\left( \begin{bmatrix} -1&1&-1&0&1\\ 1&1&1&-1&0\\ 1&1&-1&-1&0 \end{bmatrix} \circ \begin{bmatrix} 1&4&2&1&1\\ 6&1&7&3&1\\ 4&1&2&5&1 \end{bmatrix} \right) \begin{bmatrix} x_1\\ x_2 \end{bmatrix} ^{\left[ {\begin{matrix} 5 &{} 0\\ 2 &{} 1\\ 2 &{} 0\\ 0 &{} 3\\ 0 &{} 2 \end{matrix}}\right] }.$$
This concludes our example.
In general, a system $$\hat{f}\in \mathbb {R}[x_1,\dots ,x_d]^u$$ of multivariate polynomials over the reals will be written compactly as
$$\hat{f}=(s\circ \hat{c}) x^{e},$$
where We call $$s\in \{ -1,0,1\}^{u\times v}$$ the sign matrix, $$\hat{c}\in \mathbb {R}_{+}^{u\times v}$$ the coefficient matrix, and $$e\in \mathbb {N}^{v\times d}$$ the exponent matrix of $$\hat{f}$$. The rows of the exponent matrix are named $$e_1$$,..., $$e_v$$.

3 Main Result

Definition 2

(Signed Parametric Systems). A signed parametric system is given by
$$f=(s\circ c) x^{e},$$
where the sign matrix $$s\in \{-1,0,1\}^{u\times v}$$ and the exponent matrix $$e\in \mathbb {N}^{v\times d}$$ are specified but the coefficient matrix c is unspecified in the sense that it is left parametric. Formally, c is a $$u\times v$$-matrix of pairwise different indeterminates.

When names of parameters and indeterminates are not important, signed parametric systems are uniquely determined by the sign matrix s and the exponent matrix e.

Example 3

The following is a signed parametric system derived from the system in Example 1:
$$\begin{bmatrix} f_{1}\\ f_{2}\\ f_{3} \end{bmatrix} =\left( \begin{bmatrix} -1&1&-1&0&1\\ 1&1&1&-1&0\\ 1&1&-1&-1&0 \end{bmatrix} \circ \begin{bmatrix} c_{11}&c_{12}&c_{13}&c_{14}&c_{15}\\ c_{21}&c_{22}&c_{23}&c_{24}&c_{25}\\ c_{31}&c_{32}&c_{33}&c_{34}&c_{35} \end{bmatrix} \right) \begin{bmatrix} x_1\\ x_2 \end{bmatrix} ^{\left[ {\begin{matrix} 5 &{} 0\\ 2 &{} 1\\ 2 &{} 0\\ 0 &{} 3\\ 0 &{} 2 \end{matrix}}\right] }.$$
This corresponds to
\begin{aligned} f_1&=-c_{11}x_1^5+c_{12}x_1^2x_2-c_{13}x_1^2+c_{15}x_2^2\\ f_2&= {-}c_{21}x_1^5+c_{22}x_1^2x_2+c_{23}x_1^2-c_{24}x_2^3\\ f_3&= {-}c_{31}x_1^5+c_{32}x_1^2x_2-c_{33}x_1^2-c_{34}x_2^3. \end{aligned}

Definition 4

(Parametric Positive Solutions). Consider a signed parametric system $$f=(s\circ c) x^{e}$$. A parametric positive solution of $$f(x)>0$$ is a function $$z:\mathbb {R}_+^{u\times v}\rightarrow \mathbb {R}_+^d$$ that maps each possible specification of the coefficient matrix c to a solution of the corresponding non-parametric system, i.e.,
$$\underset{c>0}{\forall }\ f\bigl (z(c)\bigr )>0.$$

Theorem 5

(Main). Let $$f=(s\circ c) x^{e}$$ be a signed parametric system. Let
$$C(n)\ :=\ \bigwedge _{i}\ \bigwedge _{s_{ik}<0}\ \bigvee _{s_{ij}>0}\ (e_{j}-e_{k}) n\ge 1.$$
Then the following are equivalent:
1. (i)

$$f(x)>0$$ has a parametric positive solution.

2. (ii)

C(n) has a solution $$n\in \mathbb {R}^{d}$$.

3. (iii)

C(n) has a solution $$n\in \mathbb {Z}^{d}$$.

In the positive case, the following function $$z$$ is a parametric positive solution of $$f(x)>0$$:
$$z(c)=t^{n},\quad \text {where}\quad t=1+\sum _{\begin{array}{c} s_{ij}>0 \\ s_{ik}<0 \end{array}}\frac{c_{ik}}{c_{ij}}.$$
In fact, we even have $$\underset{c>0}{\forall }\ \underset{r\ge t}{\forall }\ f(r^n)>0$$.

Proof

We first show that (i) implies (ii):
Assume now that (ii) holds. The existence of solutions $$n\in \mathbb {R}^d$$ and $$n\in \mathbb {Q}^d$$ of C(n) coincides due to the Linear Tarski Principle: Ordered fields admit quantifier elimination for linear formulas, and therefore $$\mathbb {Q}$$ is an elementary substructure of $$\mathbb {R}$$ with respect to linear sentences [29]. Given a solution $$n\in \mathbb {Q}^d$$, we can use the principal denominator $$\delta \ge 1$$ of all coordinates of n to obtain a solution $$\delta n\in \mathbb {Z}^d$$. Hence (iii) holds.
We finally show that (iii) implies (i):
In the proof of the implication from (iii) to (i) we have applied $$\log _t$$ so that $$n=\log _t x$$ and, accordingly, $$x=t^n$$, where t is as stated in the theorem. Notice that any larger choice $$r\ge t$$ would work there as well.    $$\square$$

Example 6

Consider with $$f_1$$, $$f_2$$ taken from Example 3:
\begin{aligned} f_1&=-c_{11}x_1^5+c_{12}x_1^2x_2-c_{13}x_1^2+c_{15}x_2^2\\ f_2&=c_{21}x_1^5+c_{22}x_1^2x_2+c_{23}x_1^2-c_{24}x_2^3. \end{aligned}
This gives us
$$s= \begin{bmatrix} -1&1&-1&0&1\\ 1&1&1&-1&0 \end{bmatrix} \quad \text {and}\quad e= \begin{bmatrix} 5&0\\ 2&1\\ 2&0\\ 0&3\\ 0&2 \end{bmatrix}.$$
We obtain C(n) as follows:
\begin{aligned}&\left( \left( \begin{bmatrix}2&1\end{bmatrix}-\begin{bmatrix}5&0\end{bmatrix}\right) n\ge 1\vee \left( \begin{bmatrix}0&2\end{bmatrix}-\begin{bmatrix}5&0\end{bmatrix}\right) n\ge 1\right) \wedge {}\\&\left( \left( \begin{bmatrix}2&1\end{bmatrix}-\begin{bmatrix}2&0\end{bmatrix}\right) n\ge 1\vee \left( \begin{bmatrix}0&2\end{bmatrix}-\begin{bmatrix}2&0\end{bmatrix}\right) n\ge 1\right) \wedge {}\\&\left( \left( \begin{bmatrix}5&0\end{bmatrix}-\begin{bmatrix}0&3\end{bmatrix}\right) n\ge 1\vee \left( \begin{bmatrix}2&1\end{bmatrix}-\begin{bmatrix}0&3\end{bmatrix}\right) n\ge 1\vee \left( \begin{bmatrix}2&0\end{bmatrix}-\begin{bmatrix}0&3\end{bmatrix}\right) n\ge 1\right) , \end{aligned}
which simplifies to
\begin{aligned}&(\begin{bmatrix}-3&1\end{bmatrix}n\ge 1 \vee \begin{bmatrix}-5&2\end{bmatrix} n\ge 1)\wedge (\begin{bmatrix}0&1\end{bmatrix} n\ge 1 \vee \begin{bmatrix}-2&2\end{bmatrix} n\ge 1)\wedge {}\\&\quad \quad \quad \quad \quad \qquad \qquad \qquad \qquad (\begin{bmatrix}5&-3\end{bmatrix}n\ge 1 \vee \begin{bmatrix}2&-2\end{bmatrix} n\ge 1 \vee \begin{bmatrix}2&-3\end{bmatrix} n\ge 1). \end{aligned}
This straightforwardly yields the input file shown in Fig. 1. It uses the standardized SMT-LIB language [4] so that it can be directly processed by highly optimized SMT solvers like CVC4 [3], MathSat [12], SMT-RAT [15], Yices [19], or Z3 [16]. All these tools certify satisfiability and give a possible solution for n, which is called a model in the SMT world:
$$n=\begin{bmatrix}-\frac{5}{2}\\-2\end{bmatrix}.$$
Hence $$(s\circ c) x^{e}>0$$ has a parametric positive solution, e.g.,
\begin{aligned} z(c) = \begin{bmatrix} t^{-\frac{5}{2}}\\ t^{-2} \end{bmatrix}, \quad \text {where}\quad \displaystyle t=1+\frac{c_{11}}{c_{12}}+ \frac{c_{11}}{c_{15}}+\frac{c_{13}}{c_{12}}+\frac{c_{13}}{c_{15}}+\frac{c_{24}}{c_{21}}+ \frac{c_{24}}{c_{22}}+\frac{c_{24}}{c_{23}}. \end{aligned}
With this solution, in particular the non-parametric subsystem of Example 1 is feasible. If $$\hat{c}$$ denotes the coefficient matrix there, then we can compute $$t=\frac{719}{28}$$ and
\begin{aligned} z(\hat{c})= \begin{bmatrix} \frac{784\sqrt{20132}}{371694959}\\[1ex] \frac{1568}{516961}\\ \end{bmatrix} \approx \begin{bmatrix} 0.0003\\ 0.0015 \end{bmatrix}. \end{aligned}
Fig. 2 illustrates the situation.

Example 7

We slightly modify Example 6 and consider the subsystem $$\left[ {\begin{matrix} f_{1}\\ f_{3} \end{matrix}}\right]$$ of Example 3:
\begin{aligned} f_1&=-c_{11}x_1^5+c_{12}x_1^2x_2-c_{13}x_1^2+c_{15}x_2^2\\ f_3&=c_{31}x_1^5+c_{32}x_1^2x_2-c_{33}x_1^2-c_{34}x_2^3. \end{aligned}
That is
$$s= \begin{bmatrix} -1&1&-1&0&1\\ 1&1&-1&-1&0 \end{bmatrix},\quad e= \begin{bmatrix} 5&0\\ 2&1\\ 2&0\\ 0&3\\ 0&2 \end{bmatrix}.$$
Computing C(n) and generating SMT-LIB input analogously to Example 6, SMT solvers will return “unsat,” which means that C(n) does not have a solution $$n\in \mathbb {R}^{2}$$. Hence $$( s\circ c) x^{e} > 0$$, i.e. $$f_1>0$$, $$f_3>0$$, does not have a parametric positive solution.
Nevertheless, with the concrete instantiations $$\hat{f}_1$$, $$\hat{f}_3$$ from Example 1 the corresponding system $$\hat{f}_1>0$$, $$\hat{f}_3>0$$ of inequalities is feasible in $$\mathbb {R}_+^2$$. One possible solution is
\begin{aligned} \begin{bmatrix} \frac{3}{2}\\ \frac{3}{2} \end{bmatrix}. \end{aligned}
However, if we change the absolute value of the leading coefficient of $$\hat{f}_1$$ from 1 to 4 yielding $$\hat{f}_1^*=-4x_1^5+4x_1^2x_2-2x_1^2+x_2^2$$, then $$\hat{f}_1^*>0$$, $$\hat{f}_3>0$$ is infeasible in $$\mathbb {R}_+^2$$. Figure 2 illustrates the situation.

4 A Re-analysis of Subtropical Methods

For non-parametric systems of real polynomial inequalities, heuristic Newton polytope-based subtropical methods [22, 37] have been successfully applied in two quite different areas: Firstly, qualitative analysis of biological and chemical networks and, secondly, SMT solving.

In the first area, a positive solution of a very large single inequality could be computed. The left hand side polynomial there has more than $$8\cdot 10^5$$ monomials in 10 variables with individual degrees up to 10. This computation was the hard step in finding an exact positive solution of the corresponding equation using a known positive point with negative value of the polynomial and applying the intermediate value theorem. To give a very rough idea of the biological background: The polynomial is a Hurwitz determinant originating from a system of ordinary differential equations modeling mitogen-activated protein kinase (MAPK) in the metabolism of a frog. Positive zeros of the Hurwitz determinant point at Hopf bifurcations, which are in turn indicators for possible oscillation of the corresponding reaction network. For further details see [21].

In the second area, a subtropical approach for systems of several polynomial inequalities has been integrated with the SMT solver veriT [6]. That incomplete combination could solve a surprisingly large percentage of SMT benchmarks very fast and thus establishes an interesting heuristic preprocessing step for SMT solving over quantifier-free nonlinear arithmetic (QF_NRA). For detailed statistics see [22].

The goal of this section is to make precise the connections between subtropical methods and our main result here, to use these connections to improve the subtropical methods, and to precisely characterize their incompleteness.

4.1 Subtropical Real Root Finding

In [37] we have studied an incomplete method for heuristically finding a positive solution for a single multivariate polynomial inequality with fixed integer coefficients:
\begin{aligned}{}[\hat{f}_1] = (s\circ \hat{c})x^{e}\quad \text {where}\quad s\in \{-1,0,1\}^{1\times v},\quad \hat{c}\in \mathbb {Z}_+^{1\times v},\quad e\in \mathbb {N}^{v\times d}. \end{aligned}
The method considers the positive and the negative support, which in terms of our notions is given by
\begin{aligned} S^+=\{\,e_j\mid s_{1j}>0\,\},\quad S^-=\{\,e_k\mid s_{1k}<0\,\}. \end{aligned}
Then [37, Lemma 4] essentially states that $$f_1(x)>0$$ has a positive solution if
\begin{aligned} C'\ := \bigvee _{e_j\in S^+} \ \underset{n\in \mathbb {R}^d}{\exists } \ \underset{\gamma \in \mathbb {R}}{\exists } \ \left( \begin{bmatrix}-e_j&1\end{bmatrix}\begin{bmatrix}n\\\gamma \end{bmatrix}\le -1 \wedge \bigwedge _{\begin{array}{c} e_k\in S^+\cup S^{-} \\ e_k\ne e_j \end{array}} \begin{bmatrix}e_k&-1\end{bmatrix}\begin{bmatrix}n\\\gamma \end{bmatrix}\le -1 \right) . \end{aligned}
Unfortunately, in [37, Lemma 4] vectors $$e_l=\begin{bmatrix} 0&\cdots&0\end{bmatrix}$$ corresponding to absolute summands are treated specially. We have noted already in [22, p. 192] that an inspection of the proof shows that this is not necessary. Therefore we discuss here a slightly improved and simpler version without that special treatment, which has been explicitly stated as [22, Lemma 2].
The proof of the loop invariant (I1) in [37, Theorem 5(ii)] shows that the positive support need not be considered in the conjunction:
\begin{aligned} C'\ \Longleftrightarrow \bigvee _{e_j\in S^+} \ \underset{n\in \mathbb {R}^d}{\exists } \ \underset{\gamma \in \mathbb {R}}{\exists } \ \left( \begin{bmatrix}-e_j&1\end{bmatrix}\begin{bmatrix}n\\\gamma \end{bmatrix}\le 1 \wedge \bigwedge _{e_k\in S^{-}} \begin{bmatrix}e_k&-1\end{bmatrix}\begin{bmatrix}n\\\gamma \end{bmatrix}\le -1 \right) . \end{aligned}
Starting with Fourier–Motzkin elimination [34, Sect. 12.2] of $$\gamma$$, we obtain
with C(n) as in Theorem 5.

Corollary 8

Let $$\hat{f}\in \mathbb {Z}[x_1,\dots ,x_d]$$, say, $$\hat{f}=(s\circ \hat{c})x^e$$, where $$s\in \{-1,0,1\}^{1\times v}$$, $$\hat{c}\in \mathbb {Z}_+^{1\times v}$$, $$e\in \mathbb {N}^{v\times d}$$. Let $$f=(s\circ c)x^e$$, where c is a $$1\times v$$-matrix of pairwise different indeterminates. Then the following are equivalent:
1. (i)

The algorithm find-positive [37, Algorithm 1] does not fail, and thus finds a rational solution of $$\hat{f}>0$$ with positive coordinates.

2. (ii)
There is a row $$e_j$$ of e with $$s_{1j}>0$$ such that the following LP problem has a solution $$n\in \mathbb {Q}^d$$:
\begin{aligned} \bigwedge _{s_{1k}<0} (e_j-e_k) n \ge 1. \end{aligned}

3. (iii)

$$f>0$$ has a parametric positive solution.

In the positive case, $$\hat{f}(r^n)>0$$ for all $$r\ge 1+v\sum \limits _{s_{1k}<0}\hat{c}_{1k}$$.

Proof

The equivalence between (i), (ii), and (iii) has been derived above.

According to Theorem 5, a solution for $$\hat{f}>0$$ can be obtained by plugging $$\hat{c}$$ into the parametric positive solution $$z(c)=t^n$$ for f. Since we have positive integer coefficients, we can bound t from above as follows.
\begin{aligned} t=1+\sum \limits _{\begin{array}{c} s_{1j}>0 \\ s_{1k}<0 \end{array}}\frac{\hat{c}_{1k}}{\hat{c}_{1j}} \le 1+\sum \limits _{\begin{array}{c} s_{1j}>0 \\ s_{1k}<0 \end{array}}\frac{\hat{c}_{1k}}{1} \le 1+v\sum \limits _{s_{1k}<0}\hat{c}_{1k}. \end{aligned}

$$\square$$

In simple words the equivalence between (i) and (iii) in the corollary states the following: The incomplete heuristic [37, Algorithm 1] succeeds if and only if not only the inequality for the input polynomial has a solution as required, but also the inequality for all polynomials with the same monomials and signs of coefficients as the input polynomial.

We have added (ii) to the corollary, because we consider this form optimal for algorithmic purposes. Our special case of one single inequality allows to transform the conjunctive normal form provided by Theorem 5 into an equivalent disjunctive normal form without increasing size. This way, a decision procedure can use finitely many LP solving steps [34] instead of employing more general methods like SMT solving [32].

Finally notice that the brute force search for a suitable t in find-positive [37, Algorithm 1, l.10–12] is not necessary anymore. Our corollary computes a suitable number from the coefficients.

4.2 Subtropical Satisfiability Checking

Subsequent work [22] takes an entirely geometric approach to generalize the work in [37] from one polynomial inequality to finitely many such inequalities. Consider a system with fixed integer coefficients in our notation:
\begin{aligned} \hat{f}= \begin{bmatrix} \hat{f}_{1}\\ \vdots \\ \hat{f}_{u} \end{bmatrix} =(s\circ \hat{c})x^e,\quad \text {where}\quad s\in \{-1,0,1\}^{u\times v},\quad \hat{c}\in \mathbb {Z}_+^{u\times v},\quad e\in \mathbb {N}^{v\times d}. \end{aligned}
Then [22, Theorem 12] derives essentially the following sufficient condition for the existence of a positive solution of $$\hat{f}>0$$:
\begin{aligned} C'' \ := \underset{n\in \mathbb {R}^d}{\exists } \ \underset{\gamma _1\in \mathbb {R}}{\exists }\dots \underset{\gamma _u\in \mathbb {R}}{\exists } \ \bigwedge _{i=1}^u \ \left( \left( \bigvee _{s_{ij}>0}e_{j}n+\gamma _i>0 \right) \wedge \bigwedge _{s_{ik}<0}e_{k}n+\gamma _i<0 \right) . \end{aligned}
After an equivalence transformation, we can once more apply Fourier–Motzkin elimination [34, Sect. 12.2]:
with C(n) as in Theorem 5.

Corollary 9

Let $$\hat{f}\in \mathbb {Z}[x_1,\dots ,x_d]^u$$, say, $$\hat{f}=(s\circ \hat{c})x^e$$, where $$s\in \{-1,0,1\}^{u\times v}$$, $$\hat{c}\in \mathbb {Z}_+^{u\times v}$$, $$e\in \mathbb {N}^{v\times d}$$. Let $$f=(s\circ c)x^e$$, where c is a $$u\times v$$-matrix of pairwise different indeterminates. Then the following are equivalent:
1. (i)

The incomplete subtropical satisfiability checking method for several inequalities over QF_NRA (quantifier-free nonlinear real arithmetic) introduced in [22] succeeds on $$\hat{f}>0$$.

2. (ii)
The following SMT problem with unknowns n is satisfiable over QF_LRA (quantifier-free linear real arithmetic):
\begin{aligned} \bigwedge _{i=1}^u \ \bigwedge _{s_{ik}<0} \ \bigvee _{s_{ij}>0} \ (e_{j}-e_k) n\ge 1. \end{aligned}

3. (iii)

$$f>0$$ has a parametric positive solution.

In the positive case, $$\hat{f}(r^n)>0$$ for all $$r\ge 1+v\sum \limits _{s_{ik}<0}\hat{c}_{ik}$$.

Proof

The equivalence between (i), (ii), and (iii) has been derived above. About the solution r see the proof of Corollary 8.    $$\square$$

The equivalence between (i) and (iii) in the corollary states the following: The procedure in [22] yields “sat” in contrast to “unknown” if and only if not only the input system is satisfiable, but that system with all real choices of coefficients with the same signs as in the input system. While there are no formal algorithms in [22], the work has been implemented within a combination of the veriT solver [6] with the library STROPSAT [22]. Our characterization applies in particular to the completeness of this software.

We have added (ii) to the corollary, because we consider this form optimal for algorithmic purposes. Like the original input $$C''$$ used in [22] this is a conjunctive normal form, which is ideal for DPLL-based SMT solvers [32]. Recall that u is the number of inequalities in the input, and d is the number of variables. Let $$\iota$$ and $$\kappa$$ be the numbers of positive and negative coefficients, respectively. Then compared to [22] we have reduced $$d+u$$ variables to d variables, and we have reduced $$u\kappa$$ clauses with $$\iota$$ atoms each plus u unit clauses to some different $$u\kappa$$ clauses with $$\iota$$ atoms each but without any additional unit clauses.

With the :produce-models option the SMT-LIB standard [4] supports the computation of a suitable n in (ii), from which one can compute $$r^n$$ using the bound at the end of the corollary. The work in [22] does not address the computation of solutions. It only mentions that sufficiently large r will work, which implicitly suggests a brute-force search like the one in [37, Algorithm 1, l.10–12].

Notes

Acknowledgments

This work has been supported by the European Union’s Horizon 2020 research and innovation program under grant agreement No. H2020-FETOPEN-2015-CSA 712689 SC-SQUARE and by the bilateral project ANR-17-CE40-0036 and DFG-391322026 SYMBIONT. The second author would like to thank Georg Regensburger for his hospitality and an interesting week of inspiring discussions around the topic, and Dima Grigoriev for getting him started on the subject.

References

1. 1.
Ábrahám, E.: $${\sf SC}^{\sf 2}$$: satisfiability checking meets symbolic computation. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 28–43. Springer, Cham (2016).
2. 2.
Arnon, D.S.: Algorithms for the geometry of semi-algebraic sets. Ph.D. thesis. Technical report 436, Computer Science Department, University of Wisconsin-Madison (1981)Google Scholar
3. 3.
Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011).
4. 4.
Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017)Google Scholar
5. 5.
Basu, S., Pollack, R., Roy, M.F.: On the combinatorial and algebraic complexity of quantifier elimination. JACM 43(6), 1002–1045 (1996).
6. 6.
Bouton, T., Caminha B. de Oliveira, D., Déharbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151–156. Springer, Heidelberg (2009).
7. 7.
Bradford, R.: A case study on the parametric occurrence of multiple steady states. In: Burr, M. (ed.) Proceedings of the ISSAC 2017, pp. 45–52. ACM, New York (2017).
8. 8.
Brown, C.W.: Improved projection for CAD’s of $$\mathbb{R}^3$$. In: Traverso, C. (ed.) Proceedings of the ISSAC 2000, pp. 48–53. ACM, New York (2000).
9. 9.
Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bull. 37(4), 97–108 (2003).
10. 10.
Canny, J.: Some algebraic and geometric computations in PSPACE. In: Simon, J. (ed.) Proceedings of the STOC 1988, pp. 460–467. ACM, New York (1988).
11. 11.
Chen, C., Davenport, J.H., May, J.P., Moreno Maza, M., Xia, B., Xiao, R.: Triangular decomposition of semi-algebraic systems. J. Symb. Comput. 49, 3–26 (2013).
12. 12.
Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013).
13. 13.
Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12(3), 299–328 (1991).
14. 14.
Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975).
15. 15.
Corzilius, F., Kremer, G., Junges, S., Schupp, S., Ábrahám, E.: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 360–368. Springer, Cham (2015).
16. 16.
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).
17. 17.
Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Gutierrez, J. (ed.) Proceedings of the ISSAC 2004, pp. 111–118. ACM, New York (2004).
18. 18.
Dolzmann, A., Sturm, T.: REDLOG: computer algebra meets computer logic. ACM SIGSAM Bull. 31(2), 2–9 (1997).
19. 19.
Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014).
20. 20.
England, M., Errami, H., Grigoriev, D., Radulescu, O., Sturm, T., Weber, A.: Symbolic versus numerical computation and visualization of parameter regions for multistationarity of biological networks. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2017. LNCS, vol. 10490, pp. 93–108. Springer, Cham (2017).
21. 21.
Errami, H., Eiswirth, M., Grigoriev, D., Seiler, W.M., Sturm, T., Weber, A.: Detection of Hopf bifurcations in chemical reaction networks using convex coordinates. J. Comput. Phys. 291, 279–302 (2015).
22. 22.
Fontaine, P., Ogawa, M., Sturm, T., Vu, X.T.: Subtropical satisfiability. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 189–206. Springer, Cham (2017).
23. 23.
González-Vega, L.: A combinatorial algorithm solving some quantifier elimination problems. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, pp. 365–375. Springer, Vienna (1998).
24. 24.
Grigoriev, D., Vorobjov, N.: Solving systems of polynomial inequalities in subexponential time. J. Symb. Comput. 5(1–2), 37–64 (1988).
25. 25.
Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: Watanabe, S., Nagata, M. (eds.) Proceedings of the ISSAC 1990, pp. 261–264. ACM, New York (1990).
26. 26.
Hong, H.: Improvements in CAD-based quantifier elimination. Ph.D. thesis, The Ohio State University (1990)Google Scholar
27. 27.
Hong, H., Din, M.S.E.: Variant quantifier elimination. J. Symb. Comput. 47(7), 883–901 (2012).
28. 28.
Košta, M.: New concepts for real quantifier elimination by virtual substitution. Doctoral dissertation, Saarland University, Germany (2016). https://doi.org/10.22028/D291-26679
29. 29.
Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450–462 (1993).
30. 30.
McCallum, S.: An improved projection operator for cylindrical algebraic decomposition. Ph.D. thesis, University of Wisconsin-Madison (1984)Google Scholar
31. 31.
Müller, S., Feliu, E., Regensburger, G., Conradi, C., Shiu, A., Dickenstein, A.: Sign conditions for injectivity of generalized polynomial maps with applications to chemical reaction networks and real algebraic geometry. Found. Comput. Math. 16(1), 66–97 (2016).
32. 32.
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). JACM 53(6), 937–977 (2006).
33. 33.
Renegar, J.: On the computational complexity and geometry of the first-order theory of the reals. Part II: the general decision problem. Preliminaries for quantifier elimination. J. Symb. Comput. 13(3), 301–328 (1992).
34. 34.
Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1986)
35. 35.
Strzebonski, A.: Cylindrical algebraic decomposition using validated numerics. J. Symb. Comput. 41(9), 1021–1038 (2006).
36. 36.
Sturm, T.: Real quantifier elimination in geometry. Doctoral dissertation, University of Passau, Germany (1999)Google Scholar
37. 37.
Sturm, T.: Subtropical real root finding. In: Yokoyama, K., Linton, S., Robertz, D. (eds.) Proceedings of the ISSAC 2015, pp. 347–354. ACM, New York (2015).
38. 38.
Tarski, A.: The Completeness of Elementary Algebra and Geometry. Institute Blaise Pascal, Paris (1930). Reprinted by CNRS 1967Google Scholar
39. 39.
Viro, O.: Dequantization of real algebraic geometry on logarithmic paper. CoRR arXiv:math/0005163 (2000)
40. 40.
Weber, A., Sturm, T., Abdel-Rahman, E.O.: Algorithmic global criteria for excluding oscillations. Bull. Math. Biol. 73(4), 899–916 (2011).
41. 41.
Weispfenning, V.: A new approach to quantifier elimination for real algebra. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, pp. 376–392. Springer, Vienna (1998).
42. 42.
Wolfram, S.: The Mathematica Book, 5th edn. Cambridge University Press, Cambridge (2003)
43. 43.
Yanami, H., Anai, H.: SyNRAC: a Maple toolbox for solving real algebraic constraints. In: Dolzmann, A., Seidl, A., Sturm, T. (eds.) Proceedings of the A3L 2005, pp. 275–279. BoD, Norderstedt (2005)Google Scholar

Authors and Affiliations

• Hoon Hong
• 1
• Thomas Sturm
• 2
• 3
1. 1.North Carolina State UniversityRaleighUSA
2. 2.CNRS, Inria, and the University of LorraineNancyFrance
3. 3.MPI Informatics and Saarland UniversitySaarbrückenGermany