Thomas Sturm
email: thomas@thomas-sturm.de

Thirty Years of Virtual Substitution Foundations, Techniques, Applications

Keywords: Computing methodologies → Equation and inequality solving algorithms, Algebraic algorithms, Real quantifier elimination, virtual substitution

In 1988, Weispfenning published a seminal paper introducing a substitution technique for quantifier elimination in the linear theories of ordered and valued fields. The original focus was on complexity bounds including the important result that the decision problem for Tarski Algebra is bounded from below by a double exponential function. Soon after, Weispfenning's group began to implement substitution techniques in software in order to study their potential applicability to real world problems. Today virtual substitution has become an established computational tool, which greatly complements cylindrical algebraic decomposition. There are powerful implementations and applications with a current focus on satisfiability modulo theory solving and qualitative analysis of biological networks.

∃x∀y(p ≤ 0 ∨ q > 0). When a ≥ 0, we can choose x = -b + 1 to satisfy q > 0. When b ≤ 0, we can choose x = 0 to satisfy p ≤ 0. Thus a ≥ 0 ∨ b ≤ 0 implies ¬φ. Equivalently, φ implies

φ ′ = a < 0 ∧ b > 0.
Vice versa, it is not too hard to see that φ ′ also implies φ.

Formally, we are considering interpreted first-order logic with equality over a finite language L = (0, 1, +, -, •, =, ≤, <, ) where all symbols have their usual interpretations over the reals. We assume w.l.o.g. that L-formulas are in prenex normal form

φ = Q n x n . . . Q 1 x 1 ψ , Q i ∈ {∃, ∀}, ψ quantifier-free.
If all variables occurring in ψ are quantified, in other words, if there are no parameters, φ is called an L-sentence.

Given a first-order L-formula φ, real quantifier elimination (QE) computes a quantifier-free L-formula φ ′ such that

R |= φ ←→ φ ′ .
When applying quantifier elimination to a sentence φ, the obtained quantifier-free formula φ ′ will not contain any variables and can be straightforwardly evaluated to either "true" or "false. " This way, real quantifier elimination establishes in particular a decision procedure.

HISTORY AND SCIENTIFIC CONTEXT

The first real quantifier elimination procedure was developed by Tarski around 1930 [START_REF] Tarski | The Completeness of Elementary Algebra and Geometry[END_REF] but, due to the war, published only in 1948 [START_REF] Tarski | A Decision Method for Elementary Algebra and Geometry[END_REF]. Tarski's procedure is not elementary recursive. As early as 1954, concluding remarks in a technical report by Davis to the US Army on an implementation of a corresponding procedure for Presburger arithmetic point at a surprisingly early interest in software implementations also of real quantifier elimination [START_REF] Davis | Final Report on Mathematical Procedures for Decision Problems[END_REF].

During the 1970s, Collins developed the first elementary recursive real quantifier elimination procedure [START_REF] Collins | Quantifier Elimination for the Elementary Theory of Real Closed Fields by Cylindrical Algebraic Decomposition[END_REF], which was based on cylindrical algebraic decomposition (CAD). An implementation by Arnon was available around 1980 [START_REF] Arnon | Algorithms for the Geometry of Semi-Algebraic Sets[END_REF]. CAD has undergone many improvements since and establishes an active research area until today [START_REF] Brown | Constructing a Single Cell in Cylindrical Algebraic Decomposition[END_REF][START_REF] Collins | Partial Cylindrical Algebraic Decomposition for Quantifier Elimination[END_REF][START_REF] Mccallum | An Improved Projection Operation for Cylindrical Algebraic Decomposition of Three-Dimensional Space[END_REF][START_REF] Mccallum | On Using Lazard's Projection in CAD Construction[END_REF]. The method is double exponential, more precisely double exponential in the number of all occurring variables [START_REF] Brown | The Complexity of Quantifier Elimination and Cylindrical Algebraic Decomposition[END_REF]. A robust implementation is available in the interactive system Qepcad B, originally by Hong and now developed by Brown [START_REF] Brown | QEPCAD B: A Program for Computing with Semialgebraic Sets Using CADs[END_REF].

From the mid 1980s to the early 1990s there was a strong interest in the asymptotic worst-case time complexity of the real decision problem. In 1988, Davenport-Heintz [START_REF] Davenport | Real Quantifier Elimination is Doubly Exponential[END_REF] and Weispfenning [START_REF] Volker | The Complexity of Linear Problems in Fields[END_REF] independently showed that it is doubly exponential. Weispfenning's article actually brought even stronger results: First, it showed that the decision problem is doubly exponential already for linear formulas, where there are no products between variables. Next, considering finer complexity parameters than the input word length it Invited Talk ISSAC '18, July 16-19, 2018, New York, NY, USA

showed that the problem for linear formulas is doubly exponential only in the number of quantifier alternations. Finally, it came with a corresponding quantifier elimination procedure, where the idea is for the elimination of an existential quantifier to formally substitute sufficiently many test terms derived from parametric zeros of polynomials contained in the input formula. Subsequent research on complexity by Grigoriev, Renegar, Basu-Pollack-Roy, and others developed entirely new real quantifier elimination procedures with strong theoretical results taking into consideration even finer complexity parameters like polynomial degrees or coefficient sizes [START_REF] Basu | On the Combinatorial and Algebraic Complexity of Quantifier Elimination[END_REF][START_REF] Grigoriev | Complexity of Deciding Tarski Algebra[END_REF][START_REF] Renegar | On the Computational Complexity and Geometry of the First-Order Theory of the Reals[END_REF].

Virtual substitution was implemented by Weispfenning's students in the computer logic system Redlog [START_REF] Dolzmann | Redlog: Computer Algebra Meets Computer Logic[END_REF][START_REF] Dolzmann | Redlog User Manual, 2nd Edition[END_REF][START_REF] Sturm | New Domains for Applied Quantifier Elimination[END_REF][START_REF] Sturm | REDLOG Online Resources for Applied Quantifier Elimination[END_REF], which developed into an established tool with about 400 citations in the scientific literature pointing at quite a number of successful applications, mostly in the sciences. Such implementations require powerful heuristics, which by themselves establish significant research in symbolic computation [START_REF] Dolzmann | Algorithmic Strategies for Applicable Real Quantifier Elimination[END_REF][START_REF] Dolzmann | Approaches to Parallel Quantifier Elimination[END_REF][START_REF] Dolzmann | Simplification of Quantifier-free Formulae over Ordered Fields[END_REF][START_REF] Dolzmann | A New Approach for Automatic Theorem Proving in Real Geometry[END_REF][START_REF] Korovin | Towards Conflict-Driven Learning for Virtual Substitution[END_REF][START_REF] Košta | Better Answers to Real Questions[END_REF][START_REF] Sturm | Real Quantifier Elimination in Geometry[END_REF][START_REF] Sturm | Verification and Synthesis Using Real Quantifier Elimination[END_REF][START_REF] Sturm | Investigating Generic Methods to Solve Hopf Bifurcation Problems in Algebraic Biology[END_REF][START_REF] Sturm | Investigating Algebraic and Logical Algorithms to Solve Hopf Bifurcation Problems in Algebraic Biology[END_REF]. As the above-mentioned complexity results suggest, the focus is on problems with few quantifier alternations and with parameters.

We are going to discuss the development of virtual substitution from a linear method to higher degrees, which went surprisingly slow. This was caused by several factors. First, motivated by the success with real quantifier elimination, there was a focus on research on virtual substitution for various other theories, which we will address in Section 8. Second, from a practical point of view, plenty of meaningful problems have been solved with a degree bound of only 2. Third, on the one hand, the question for higher degrees had been theoretically answered already in 1997 [START_REF] Volker | Quantifier Elimination for Real Algebra-the Quadratic Case and Beyond[END_REF], and, on the other hand, there was a strong belief that with higher degrees practical implementations would be outperformed by CAD. Recent work by Košta and his accompanying implementation paint a more positive picture [START_REF] Košta | New Concepts for Real Quantifier Elimination by Virtual Substitution[END_REF].

THE LINEAR CASE FOR THE REALS

We start with Weispfenning's original result from 1988 [START_REF] Volker | The Complexity of Linear Problems in Fields[END_REF]. Elimination takes place in an extended language L ′ = L ∪ {inv} with a unary function symbol inv for multiplicative inverses. In order to avoid partial functions, one defines in the L ′ -structure R that inv(0) = 0. Notice that, e.g., 2a 2 b inv(2a 3 ) = ab inv(a 2 ) but one cannot further reduce to lowest terms without a case distinction on the vanishing of a. An L ′ -formula φ is called a linear in x 1 , . . . , x n if it contains no products or multiplicative inverses of the x i . Coefficients of the x i are arbitrary L ′ -terms in the parameters. We use ± as a shorthand for listing multiple terms. Theorem 3.1 (Linear real QE; Weispfenning, 1988). Let ψ be a quantifier-free L ′ -formula linear in variables x 1 , . . . , x n . Write the set of atomic formulas occurring in ψ as

Ψ = { a j x 1 + b j ϱ j 0 | j ∈ J },
where J is a finite index set, a j , b j are L ′ -terms not containing x 1 , and ϱ j are relations from L ′ .

Sk(x 1 , Ψ) = -b j inv(a j )±1, -b j inv(2a j )-b k inv(2a k ) j, k ∈ J .
Then the following holds:

(i) Fix real interpretations for all variables except x 1 . Then for each interpretation of x 1 in R there is at least one t ∈ Sk(x 1 , Ψ) such that all atomic formulas in Ψ evaluate identically for the considered interpretation of x 1 and t:

R |= ∀x 1 t ∈Sk(x 1 , Ψ) ψ ∈Ψ ψ ←→ ψ [x 1 /t] .
(ii) This allows quantifier elimination of the innermost quantifier

Q 1 x 1 from Q n x n . . . Q 1 x 1 ψ : R |= ∃x 1 ψ ←→ t ∈Sk(x 1 , Ψ) ψ [x 1 /t] R |= ∀x 1 ψ ←→ t ∈Sk(x 1 , Ψ) ψ [x 1 /t].
(iii) The elimination results on the right hand sides of the bi-implications in (ii) are linear in x 2 , . . . , x n . Hence the theorem can be iteratively applied to

Q 2 x 2 , . . . , Q n x n . □ For j = k we have in particular -b j inv(a j ) ∈ Sk(x 1 , Ψ). The set Sk(x 1 , Ψ) is called a Skolem set, where Theorem 3.1(i) is the defining property of Skolem sets.
Consider the application of Theorem 3.1 for the elimination of several subsequent existential quantifiers. We can exploit the compatibility of existential quantifiers with logical disjunction to move subsequent quantifiers inside the disjunctions after each elimination step:

∃x 2 ∃x 1 ψ ←→ ∃x 2 t ψ [x 1 /t] ←→ t ∃x 2 ψ [x 1 /t].
The same works with universal quantifiers and conjunctions. This observation has been made for Presburger arithmetic already by Reddy-Loveland in 1978 [START_REF] Cattamanchi | Presburger Arithmetic with Bounded Quantifier Alternation[END_REF]. In our situation we obtain # Sk(x 1 , Ψ) many independent elimination steps for ∃x 2 , where Skolem sets will be smaller and, more important, the terms of each Skolem set must be substituted only into the corresponding member of the disjunction. Whenever there is a quantifier alternation, i.e., a change between ∃ and ∀ in the prenex block, we will encounter ∀ in front of a disjunction or ∃ in front of a conjunction, and our optimization is not applicable. Theorem 3.2 (Complexity, Weispfenning 1988). Consider a prenex linear formula φ = Q n x n . . . Q 1 x 1 ψ . Let a be the number of quantifier alternations, and let b be the longest occurring sequence of quantifiers without alternation. Denote by T (length(φ)) the time asymptotically required for the elimination of all quantifiers from φ using Theorem 3.1 as described. Then the following holds:

(i) T (length(φ)) = 2 ↑ 2 ↑ O(length(φ)
). This bound is tight in the sense that the corresponding time complexity of the problem is bounded from below by a function in

2 ↑ 2 ↑ Ω(length(φ)). (ii) If a is bounded, then T (length(φ)) = 2 ↑ O(length(φ)).
(iii) Assume that both a and b are bounded, say a ≤ α and b ≤ β.

Then T (length(φ)) = length(φ) ↑ (α + 1)O(β) α +1 . This applies in particular if n is bounded.

Proof. The proof of the upper bounds is based on the following observations. For a term t = a 0 + n i=1 a i x i define rank(t) = max n i=0 length(a i ), which naturally extends to sets of atomic formulas. Then rank(Sk( The existential decision problem had been shown to be in NP by von zur Gathen-Sieveking already in 1976 [START_REF] Von | Weitere zum Erfüllungsproblem polynomial äquivalente kombinatorische Aufgaben[END_REF]. Fourier-Motzkin elimination [START_REF] Fourier | Analyse des travaux de l'Académie Royale des Sciences pendant l'année 1824, Partie mathématique[END_REF][START_REF] Motzkin | Beiträge zur Theorie der linearen Ungleichungen[END_REF] is double exponential even without quantifier alternation. However, the single exponential complexity comes at a price. On input of a conjunction of atomic formulas, Fourier-Motzkin elimination preserves that form, while Theorem 3.1 produces a disjunction of conjunctions of atomic formulas (DNF). With a more algebraic choice of words, on input of a system of constraints, the theorem introduces unnecessary case distinctions.

x 1 , Ψ)) = O(rank(Ψ)), # Sk(x 1 , Ψ) = O(#Ψ 2 ),
Notice that Theorem 3.1 uses regular term substitution. The theorem was soon implemented in order to study its practical performance [START_REF] Burhenne | Implementierung eines Algorithmus zur Quantorenelimination für lineare reelle Probleme[END_REF]. Two problems became apparent. First, although hardly relevant from the point of view of theoretical complexity bounds, the quadratic growth of the Skolem sets with the arithmetic means, which have the purpose to cover open intervals, significantly slowed down computation times and increased result sizes. Second, results contained nested occurrences of inv, hiding case distinctions and making them hard to understand for human readers.

For the first problem one moved to another extension language L ′′ = L ′ ∪ {ε}, where ε is a constant for a positive infinitesimal, and used -b j inv(a j ) ± ε instead of -b j inv(2a j )b k inv(2a k ). The results then contained also ε, which made the second problem even worse. It turned out that both inv and ε can be equivalently removed introducing suitable quantifier-free case distinctions. The question was then whether to remove those symbols from the final result in a post-processing step, or as early as possible during elimination. The early elimination performed way better than post-processing, and lifting this observation from an implementation detail to the mathematical level was the birth of virtual substitution.

Virtual substitution does not map terms to terms but atomic formulas to quantifier-free formulas. This relaxation is surprisingly strong. It not only solves both above-mentioned problems but, as we shall see soon, allows to generalize the method from the linear case to arbitrary higher degree bounds. From now on, our language is the original language L without any extensions. As an example, we give the virtual substitution of a quotient, which is not an L-term, into a linear weak inequality. The quotient comes in a pair with a guard guaranteeing that it is defined in R. This pair is called a test point. We substitute formally and then multiply by the positive square of the denominator:

(αx 1 + β ≤ 0) x 1 a 0, -b a = a 0 ∧ -αab + βa 2 ≤ 0.
Virtual substitution of tε treats the virtual substitution of t as a black-box and takes into consideration the derivative of the targeted polynomial:

(ax 1 + b < 0)[x 1 / /(χ , t -ε)] = (ax 1 + b < 0)[x 1 / /(χ , t)] ∨ (ax 1 + b = 0)[x 1 / /(χ , t)] ∧ a > 0 .
A complete set of virtual substitutions for the linear case can be found in [START_REF] Loos | Applying Linear Quantifier Elimination[END_REF].

Since ∀x 1 ψ is equivalent to ¬∃x 1 ¬ψ , we assume w.l.o.g. that Q 1 = ∃ from now on. A positive quantifier-free L-formula is an ∧-∨-combination of atomic L-formulas. L-formulas can be efficiently made positive by moving logical negations ¬ inside via de Morgan's laws and then eliminating them in front of atomic formulas by adapting relations and signs of terms. Language allowing this, like our L, are called closed under negation. Theorem 3.3 (Improved linear real QE; [START_REF] Loos | Applying Linear Quantifier Elimination[END_REF]. Let ψ be a positive quantifier-free L-formula linear in variables x 1 , . . . , x n . Write the set of atomic formulas occurring in ψ as

Ψ = 4 k =1 { a j x 1 + b j ϱ k 0 | j ∈ J k },
where J k are finite index sets, a j , b j are L-terms not containing x 1 , and

(ϱ 1 , . . . , ϱ 4 ) = (=, ≤, <, ) are relations from L. Denote S j = - b j a j
and define

E(x 1 , Ψ) = (true, ∞) ∪ (a j 0, S j ) j ∈ J 1 ∪ J 2 ∪ (a j 0, S j -ε) j ∈ J 3 ∪ J 4 .
Then E(x 1 , Ψ) allows quantifier elimination of an innermost existential quantifier ∃x 1 from Q n x n . . . Q 2 x 2 ∃x 1 ψ via virtual substitution:

R |= ∃x 1 ψ ←→ t ∈E(x 1 , Ψ) ψ [x 1 / /t].
The elimination result on the right hand side of the bi-implication is linear in x 2 , . . . , x n so that the theorem can be iteratively applied to ∃x 2 , . . . , ∃x n .

Proof. Fix a real interpretation ι for all variables except x 1 , and consider the set

S = { r ∈ R | R, ι ∪ {x 1 = r } |= ψ } of
satisfying values with respect to ι for x 1 . If S = ∅, then there is nothing to prove. Otherwise E(x 1 , Ψ) must contain at least one test term t such that R, ι |= ψ [x 1 / /t]. If S is unbounded from above, then we have t = ∞. Assume now that sup S = s ∈ R. If s ∈ S, then s = S j with j ∈ J 1 ∪ J 2 , and we have (true, s) ∈ E(x 1 , Ψ). If s S, then s = S j with j ∈ J 3 ∪ J 4 , and we have (true, sε) ∈ E(x 1 , Ψ). □

To illustrate the limitation to positive formulas, consider the nonpositive L-formula ∃xψ with ψ = ¬(x 0). Elimination would fail with E(x 1 , Ψ) = {(1 0, -ε), (true, ∞)} from the theorem, because ψ holds for x = 0, which is not simulated by either of the two elements of E. This also shows that E(x 1 , Ψ) is not a Skolem set.

THE QUADRATIC CASE FOR THE REALS

An L-formula φ is quadratic in x 1 if all occurring terms can be written as t = ax 2 1 + bx 1 + c, where the coefficients a, b, c are polynomials not containing x 1 . We discuss the virtual substitution of one root of such a quadratic polynomial t into an equation g = 0. Univariate division with remainder yields

g = qt + αx 1 + β, (2)
where α and β do not contain x 1 . Since we are considering a root of t, we can as well substitute into the linear remainder:

(αx 1 + β = 0) x a 0 ∧ -∆ < 0, -b+ √ ∆ 2a = (3) a 0 ∧ -∆ < 0 ∧ (-αb + 2βa) 2 = α 2 ∆ ∧ (-αb + 2βa)α ≤ 0.
To understand this substitution consider the formal substitution

α -b + √ ∆ 2a + β = (-αb + 2βa) + α √ ∆ 2a .
The L-formula in (3) expresses that the two summands of the numerator have equal absolute values and that their signs are opposite or both zero. A complete set of virtual substitutions for the quadratic case can be found in [START_REF] Volker | Quantifier Elimination for Real Algebra-the Quadratic Case and Beyond[END_REF].

Theorem 4.1 (Quadratic real QE; Weispfenning, 1997). Let ψ be a positive quantifier-free L-formula at most quadratic in x 1 . Write the set of atomic formulas occurring in ψ as

Ψ = 4 k =1 { a j x 2 1 + b j x 1 + c j ϱ k 0 | j ∈ J k },
where J k are finite index sets, a j , b j , c j are L-terms not containing x 1 , and (ϱ 1 , . . . , ϱ 4 ) = (=, ≤, <, ) are relations from L. Denote S j = -

c j b j , ∆ j = b 2 -4ac, R ± j = -b j ± √ ∆ j 2a j
, and define

E(x 1 , Ψ) = (true, ∞) ∪ (a j 0 ∧ -∆ j ≤ 0, R ± j ), (a j = 0 ∧ b j 0, S j ) j ∈ J 1 ∪ J 2 ∪ (a j 0 ∧ -∆ j ≤ 0, R ± j -ε), (a j = 0 ∧ b j 0, S j -ε) j ∈ J 3 ∪ J 4 .
Then E(x 1 , Ψ) allows quantifier elimination of an innermost existential quantifier ∃x 1 from Q n x n . . . Q 2 x 2 ∃x 1 ψ via virtual substitution:

R |= ∃x 1 ψ ←→ t ∈E(x 1 , Ψ) ψ [x 1 / /t]. □
The proof is analogous to the proof of Theorem 3.3. However, there is no guarantee that Theorem 4.1 can be iterated. In Equation (3) above one can see that degrees are doubled within α, β, a, b, which can all contain x 2 , . . . , x n . Applying the theorem to the inner ∃y of our introductory example [START_REF] Ábrahám | SC 2 : Satisfiability Checking Meets Symbolic Computation[END_REF] we obtain in the output, e.g., ab 2 + 2abx 2 + ax 4 + bx 2 + x 3 , which is not quadratic in the universally quantified x anymore. When applying suitable simplification heuristics during elimination, input formulas modelling real world situations, in contrast to random input, are surprisingly well-behaved concerning the increase of degrees.

Against this background, theoretical complexity results would have to weigh efficiency against incompleteness. Practical computing times appear compatible with Theorem 3.2 also in the quadratic case.

HIGHER DEGREES FOR THE REALS

The real type of a polynomial is the finite sequence of the signs assumed from -∞ to ∞. For instance, x 2 1 -2 has real type (1, 0, -1, 0, 1), because both its leading coefficient and its discriminant ∆ are positive. For a generic quadratic polynomial a j x 2 1 + b j x 1 + c j there are 6 possible real types when a j does not vanish plus 2 possible real types when a j does vanish. The former are characterized by the signs of a j and ∆ j , and the latter are characterized by the sign of b j . With this intuition we replace E(x 1 , Ψ) from Theorem 4.1 with the following variant, which establishes a case distinction on real types omitting two of them with ∆ j < 0, where there are no real roots:

E ′ (x 1 , Ψ) = (true, ∞) ∪ (4) (-a j < 0 ∧ -∆ j < 0, R ± j ), (-a j < 0 ∧ ∆ j = 0, R + j ), (a j < 0 ∧ -∆ j < 0, R ± j ), (a j < 0 ∧ ∆ j = 0, R + j ), (a j = 0 ∧ -b j < 0, S j ), (a j = 0 ∧ b j < 0, S j ) j ∈ J 1 ∪ J 2 ∪
"the same with R ± jε, R + jε, and S jε for j ∈ J 3 ∪ J 4 ".

We will now discuss a degree bound of 3 in such generality that our constructions work for arbitrary degree bounds. The first ingredient is the real types. There are still only finitely many of them, for which we need quantifier-free descriptions. To understand that this is possible consider a generic polynomial f = ax 3 1 + bx 2 1 + cx 1 +d and, e.g., the real type (-1, 0, 1, 0, 1). One can easily construct a first-order formula with parameters a, . . . , d stating that f has that real type, viz. τ = ∃r 1 ∃r 2 ∀x 1 ξ , where

ξ = r 1 < r 2 ∧ (x 1 < r 1 -→ f < 0) ∧ (r 1 < x 1 < r 2 -→ 0 < f ) ∧ (x 1 = r 2 -→ f = 0) ∧ (r 2 < x 1 -→ 0 < f ).
Since Tarski gave us real quantifier elimination in 1948, we know that there is an equivalent quantifier-free description τ ′ . The second ingredient is the representation of the roots. They are simply numbered from left to right, like (τ ′ , 1) and (τ ′ , 2) in our example. The third ingredient are the virtual substitutions. Recall from our discussion of (2) in the previous section that using division with remainder we must explain virtual substitution only into atomic formulas g ϱ 0, where g = αx 2 1 + βx 1 + γ is of degree less than our bound 3. There are only finitely many such atomic formulas. Here is an example with our generic polynomials f and g:

(g < 0)[x 1 / /(f , τ ′ , 1)] = τ ′ ∧ σ ′ ,
where σ ′ is a quantifier-free equivalent of the first-order description σ = ∃r

1 ∃r 2 ∀x 1 (ξ ∧ g[x 1 /r 1 ] < 0).
Virtual substitutions for generic polynomials can be used for arbitrary polynomials as follows. Let f * , g * be polynomials of x 1degree 3 and 2, respectively. The coefficients of x 3 1 , . . . , x 0 1 in f * and g * are multivariate polynomials not containing x 1 . Let τ ′ [f /f * ] and σ ′ [f /f * , g/g * ] denote the substitution of the coefficients of f * for a, . . . , d and the coefficients of g * for α, . . . , γ . Then

(g * < 0)[x 1 / /(f * , τ ′ , 1)] = τ ′ [f /f * ] ∧ σ ′ [f /f * , g/g * ].
Theorem 5.1 (Real QE for degree bound B; Košta 2016). Let ψ be a positive quantifier-free L-formula of degree at most B in x 1 . Write the set of atomic formulas occurring in ψ as

Ψ = 4 k =1 { f j (x 1 , . . . x n , y) ϱ k 0 | j ∈ J k },
where J k are finite index sets and (ϱ 1 , . . . , ϱ 4 ) = (=, ≤, <, ) are relations from L. Let T be a finite table of quantifier-free descriptions of real types for generic polynomials up to degree B. For a type τ ∈ T let µ(τ ) be the number of distinct real roots. Let Σ = {σ ϱ ,b ,τ ,r } for

ϱ ∈ {=, ≤, <, }, 1 ≤ b ≤ B -1, τ ∈ T , 1 ≤ r ≤ µ(τ )
be another finite table. Each σ ϱ ,b ,τ ,r is a quantifier-free description of the virtual substitution of the r -th root of a generic polynomial f of type τ into g ϱ 0, where g is another generic polynomial of degree b. Define

E(x 1 ,ψ ) = (true, ∞) ∪ j ∈J 1 ∪J 2 τ ∈T 1≤r ≤µ(τ ) (f j , τ , r ) ∪ j ∈J 3 ∪J 4 τ ∈T 1≤r ≤µ(τ ) (f j , τ , r ) -ε.
Invited Talk ISSAC '18, July 16-19, 2018, New York, NY, USA Then E(x 1 , Ψ) allows quantifier elimination of an innermost existential quantifier ∃x 1 from Q n x n . . . Q 2 x 2 ∃x 1 ψ via virtual substitution:

R |= ∃x 1 ψ ←→ t ∈E(x 1 , Ψ) ψ [x 1 / /t]. □
The problem is, of course, to find suitable quantifier-free tables T and Σ. Furthermore, recall that with Equation ( 4) we have introduced case distinctions that were not necessary in Theorem 4.1. Accordingly, we actually want to find substitution formulas in Σ that work for several combinations of real types τ and root indices r simultaneously. This is known as clustering.

Košta has given such tables for B = 3, including clustering, and provided a generic implementation of Theorem 5.1, where T and Σ exist as isolated tables in software so that the implementation can be instantiated for arbitrary degree bounds without any further programming [START_REF] Košta | New Concepts for Real Quantifier Elimination by Virtual Substitution[END_REF]. Having effectively separated logic from real algebraic geometry, the development of useful tables for higher degrees is now a challenging task for the entire community in the spirit of [START_REF] Lazard | Quantifier Elimination: Optimal Solution for Two Classical Examples[END_REF], where every progress will have considerable impact for application scenarios of real quantifier elimination.

ALGORITHMS AND APPLICATIONS

There are comprehensive experiences with implementations and practical computations for various domains, where the reals clearly dominate. Such computations are feasible only in combination with fast and strong heuristics. In the first place there is simplification of quantifier-free formulas, where the central method in use is still the deep simplification from 1997, which is based on the combination of additive smart simplification with implicit theory construction during recursion [START_REF] Dolzmann | Simplification of Quantifier-free Formulae over Ordered Fields[END_REF]. Black-box/white-box simplification [START_REF] Brown | Black-Box/White-Box Simplification and Applications to Quantifier Elimination[END_REF] appears very interesting. It would be important to study how to integrate this with the current simplification framework.

Another aspect are heuristics for degree reductions. Those are equivalence transformations heuristically working against the increase of degrees with non-linear real virtual substitution, specifically polynomial factorization and degree shifts [START_REF] Dolzmann | A New Approach for Automatic Theorem Proving in Real Geometry[END_REF][START_REF] Košta | New Concepts for Real Quantifier Elimination by Virtual Substitution[END_REF][START_REF] Košta | Better Answers to Real Questions[END_REF].

Modern implementations of virtual substitution do not naively compute elimination sets from sets of atomic formulas. Instead structural elimination sets are based on prime constituents and coprime constituents. Those are arbitrary subformulas with finitely or co-finitely many solutions, respectively. Virtual substitutions are not applied to the original quantifier free formula ψ but before condensing is used to prune ψ based on the origin within ψ of the test point to be substituted [START_REF] Košta | New Concepts for Real Quantifier Elimination by Virtual Substitution[END_REF].

For an overview of applications see, e.g., [19, 25-28, 52, 53, 57-62, 68] and citations of the Redlog standard reference [START_REF] Dolzmann | Redlog: Computer Algebra Meets Computer Logic[END_REF], e.g., on Google Scholar.

IMPACT BEYOND COMPUTER ALGEBRA

Virtual substitution for the reals is well known in the satisfiability modulo theories (SMT) community. There it is typically employed in combination with DPLL(T) [START_REF] Nieuwenhuis | Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)[END_REF] as a component of theory solvers for linear and non-linear real arithmetic [START_REF] Ábrahám | SC 2 : Satisfiability Checking Meets Symbolic Computation[END_REF][START_REF] Abraham | Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework[END_REF][START_REF] Corzilius | Integrating Virtual Substitution into Strategic SMT Solving[END_REF][START_REF] Corzilius | Virtual Substitution for SMT Solving[END_REF]. Independently, Redlog took part in the SMT-COMP 2017 competition and won the section for non-linear real arithmetic using plain virtual substitution with CAD as a fallback option when exceeding the degree bound.

OTHER DOMAINS

Already in 1988, Weispfenning discussed Skolem sets for the linear theory of discretely valued fields [START_REF] Volker | The Complexity of Linear Problems in Fields[END_REF]. In 1995, an improved version using positive formulas and virtual substitution was implemented in Redlog [START_REF] Sturm | Lineare Quantorenelimination in bewerteten Körpern[END_REF]. In 1999, deep simplification for discretely valued fields was developed and implemented [START_REF] Dolzmann | P-adic Constraint Solving[END_REF]. In 2000, discrete valuations were supplemented with divisibility predicates and virtual substitution was introduced also for the linear theory of non-discretely valued fields [START_REF] Sturm | Linear Problems in Valued Fields[END_REF]. In 2001, the methods and implementations for discretely valued fields were used as a component within a solver for parametric systems of linear congruences [START_REF] Dolzmann | Parametric Systems of Linear Congruences[END_REF].

In 2002, virtual substitution was applied to term algebras over suitably expanded finite functional first-order languages [START_REF] Sturm | Quantifier Elimination in Term Algebras. The Case of Finite Languages[END_REF], equivalent to Malcev's relational expansions [START_REF] Anatolií | Axiomatizable Classes of Locally Free Algebras of Various Types[END_REF]. The complexity is in the 4th class of the Grzegorcyk hierarchy [START_REF] Grzegorczyk | Some Classes of Recursive Functions[END_REF], which is in a sense optimal, since the problem is provably not elementary recursive. The method is implemented in Redlog [START_REF] Hoffelner | Quantifier Elimination-based Parametric Solving in Term Algebras[END_REF].

In 2003, virtual substitution was applied to parametric quantified Boolean formulas (parametric QBF), i.e., propositional logic with existential and universal quantifiers over propositional variables [START_REF] Seidl | Boolean Quantification in a First-Order Context[END_REF]. The elimination sets are simply {true, false}, representing the entire finite domain. With the size of the elimination sets in O(1) the overall complexity is single exponential even with unbounded quantifier alternation. The approach and the complexity result work for all finite domains where all domain elements can be expressed as terms. This rather naive approach to propositional reasoning turns out surprisingly strong when combined with a propositional variant of the deep simplification. For certain QBF benchmarks this combination turned out even superior to adaptions of context-driven clause learning (CDCL) to QBF [START_REF] Sturm | Parametric Quantified SAT Solving[END_REF]. There is an implementation in Redlog [START_REF] Seidl | Boolean Quantification in a First-Order Context[END_REF].

During 2005-2009, there was considerable research on virtual substitution for Presburger Arithmetic with several extensions. Most of this work has been implemented in Redlog [START_REF] Lasaruk | Parametrisches Integer-Solving[END_REF][START_REF] Lasaruk | Weak Integer Quantifier Elimination Beyond the Linear Case[END_REF][START_REF] Lasaruk | Weak Quantifier Elimination for the Full Linear Theory of the Integers[END_REF][START_REF] Lasaruk | Effective Quantifier Elimination for Presburger Arithmetic with Infinity[END_REF]. In retrospect, earlier work by Weispfenning [START_REF] Volker | The Complexity of Almost Linear Diophantine Problems[END_REF] in this area and maybe even Cooper's work [START_REF] Cooper | Theorem Proving in Arithmetic without Multiplication[END_REF] already resembled virtual substitution to some extent.

and

  Invited TalkISSAC'18, July 16-19, 2018, New York, NY, USA Sk(x 1 , Ψ) can be constructed in polynomial time. The result on the lower bound requires more extensive means and is only mentioned here for its importance. □

ACKNOWLEDGMENTS

This work has been partly supported by the European Union's Horizon 2020 research and innovation programme under grant agreement No H2020-FETOPEN-2015-CSA 712689 SC-SQUARE.


Hoon Hong
email: hong@ncsu.edu

Thomas Sturm
email: thomas.sturm@loria.fr

Positive Solutions of Systems of Signed Parametric Polynomial Inequalities

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.

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 2 x 2 -c 1 x + c 0 , g(x) = -c 2 x 2 + c 1 x -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) = c1 c2 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,[START_REF] England | Symbolic versus numerical computation and visualization of parameter regions for multistationarity of biological networks[END_REF][START_REF] Errami | Detection of Hopf bifurcations in chemical reaction networks using convex coordinates[END_REF][START_REF] Weber | Algorithmic global criteria for excluding oscillations[END_REF] or Satisfiability Modulo Theories (SMT) solving [START_REF] Ábrahám | SC 2 : satisfiability checking meets symbolic computation[END_REF][START_REF] Fontaine | Subtropical satisfiability[END_REF]32]. In both these areas, one is indeed often interested in positive solutions. For instance, unknowns in the biological and chemical context of [7,[START_REF] England | Symbolic versus numerical computation and visualization of parameter regions for multistationarity of biological networks[END_REF][START_REF] Errami | Detection of Hopf bifurcations in chemical reaction networks using convex coordinates[END_REF][START_REF] Weber | Algorithmic global criteria for excluding oscillations[END_REF] 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 [START_REF] Fontaine | Subtropical satisfiability[END_REF]. 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 [START_REF] Tarski | The Completeness of Elementary Algebra and Geometry[END_REF] 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., [START_REF] Basu | On the combinatorial and algebraic complexity of quantifier elimination[END_REF][START_REF] Canny | Some algebraic and geometric computations in PSPACE[END_REF][START_REF] Collins | Quantifier elimination for real closed fields by cylindrical algebraic decompostion[END_REF][START_REF] Grigoriev | Solving systems of polynomial inequalities in subexponential time[END_REF][START_REF] Renegar | On the computational complexity and geometry of the first-order theory of the reals. Part II: the general decision problem. Preliminaries for quantifier elimination[END_REF]. Practical complexity was improved as well, often in combination with highly refined implementations, e.g., [2,[START_REF] Brown | Improved projection for CAD's of R 3[END_REF][START_REF] Chen | Triangular decomposition of semi-algebraic systems[END_REF]13,[START_REF] Dolzmann | Efficient projection orders for CAD[END_REF][START_REF] González-Vega | A combinatorial algorithm solving some quantifier elimination problems[END_REF][START_REF] Hong | An improvement of the projection operator in cylindrical algebraic decomposition[END_REF][START_REF] Hong | Improvements in CAD-based quantifier elimination[END_REF][START_REF] Hong | Variant quantifier elimination[END_REF][START_REF] Košta | New concepts for real quantifier elimination by virtual substitution[END_REF][START_REF] Mccallum | An improved projection operator for cylindrical algebraic decomposition[END_REF][START_REF] Strzebonski | Cylindrical algebraic decomposition using validated numerics[END_REF][START_REF] Sturm | Real quantifier elimination in geometry[END_REF][START_REF] Weispfenning | A new approach to quantifier elimination for real algebra[END_REF]. Today several implementations of real quantifier elimination are available in well-supported computer algebra software such as Maple [START_REF] Chen | Triangular decomposition of semi-algebraic systems[END_REF][START_REF] Yanami | SyNRAC: a Maple toolbox for solving real algebraic constraints[END_REF], Mathematica [42, later editions online], Qepcad B [START_REF] Brown | QEPCAD B: a program for computing with semi-algebraic sets using CADs[END_REF], or Reduce [START_REF] Dolzmann | REDLOG: computer algebra meets computer logic[END_REF][START_REF] Košta | New concepts for real quantifier elimination by virtual substitution[END_REF]. 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 [START_REF] Viro | Dequantization of real algebraic geometry on logarithmic paper[END_REF]. 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 [START_REF] Fontaine | Subtropical satisfiability[END_REF][START_REF] Sturm | Subtropical real root finding[END_REF]: We provide a precise characterization of their incompleteness in terms of the existence of parametric positive solutions for the originally nonparametric 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 [START_REF] Müller | Sign conditions for injectivity of generalized polynomial maps with applications to chemical reaction networks and real algebraic geometry[END_REF].

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 [START_REF] Fontaine | Subtropical satisfiability[END_REF][START_REF] Sturm | Subtropical real root finding[END_REF].

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 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:

f1 = -x 5 1 + 4x 2 1 x 2 -2x 2 1 + x 2 2 f2 = 6x 5 1 + x 2 1 x 2 + 7x 2 1 -3x 3 2 f3 = 4x 5 1 + x 2 1 x 2 -2x 2 1 -5x 3 2 .
We rewrite those polynomials by aligning their signs, coefficients, and monomial support:

f1 = -1 • 1 • x 5 1 x 0 2 + 1 • 4 • x 2 1 x 1 2 + -1 • 2 • x 3 1 x 0 2 + 0 • 1 • x 2 1 x 0 2 + 1 • 1 • x 0 1 x 2 2 f2 = 1• 6 • x 5 1 x 0 2 + 1 • 1 • x 2 1 x 1 2 + 1 • 7 • x 3 1 x 0 2 + -1 • 3 • x 2 1 x 0 2 + 0 • 1 • x 0 1 x 2 2 f3 = 1• 4 • x 5 1 x 0 2 + 1 • 1 • x 2 1 x 1 2 + -1 • 2 • x 3 1 x 0 2 + -1 • 5 • x 2 1 x 0 2 + 0 • 1 • x 0 1 x 2 2 ,
where signs are represented by -1, 0, and 1. Note that we are writing 0 coefficients as 0 • 1 for notational uniformity. Rewriting this in matrix-vector notation, we have

⎡ ⎣ f1 f2 f3 ⎤ ⎦ = ⎛ ⎝ ⎡ ⎣ -1 1 -1 0 1 1 1 1 -1 0 1 1 -1 -1 0 ⎤ ⎦ • ⎡ ⎣ 1 4 2 1 1 6 1 7 3 1 4 1 2 5 1 ⎤ ⎦ ⎞ ⎠ ⎡ ⎢ ⎢ ⎢ ⎢ ⎣ x 5 1 x 0 2 x 2 1 x 2 x 2 1 x 0 2 x 0 1 x 3 2 x 0 1 x 2 2 ⎤ ⎥ ⎥ ⎥ ⎥ ⎦
, where • is the component-wise Hadamard product. Pushing this even further, we finally obtain

⎡ ⎣ f1 f2 f3 ⎤ ⎦ = ⎛ ⎝ ⎡ ⎣ -1 1 -1 0 1 1 1 1 -1 0 1 1 -1 -1 0 ⎤ ⎦ • ⎡ ⎣ 1 4 2 1 1 6 1 7 3 1 4 1 2 5 1 ⎤ ⎦ ⎞ ⎠ x 1 x 2 ⎡ ⎢ ⎣ 5 0 2 1 2 0 0 3 0 2 ⎤ ⎥ ⎦ .
This concludes our example.

In general, a system f ∈ R[x 1 , . . . , x d ] u of multivariate polynomials over the reals will be written compactly as

f = (s • ĉ)x e , where f = ⎡ ⎢ ⎣ f1 . . . fu ⎤ ⎥ ⎦, s = ⎡ ⎢ ⎣ s 11 • • • s 1v . . . . . . s u1 • • • s uv ⎤ ⎥ ⎦, ĉ = ⎡ ⎢ ⎣ ĉ11 • • • ĉ1v . . . . . . ĉu1 • • • ĉuv ⎤ ⎥ ⎦, x = ⎡ ⎢ ⎣ x 1 . . . x d ⎤ ⎥ ⎦, e = ⎡ ⎢ ⎣ e 1 . . . e v ⎤ ⎥ ⎦ = ⎡ ⎢ ⎣ e 11 • • • e 1d . . . . . . e v1 • • • e vd ⎤ ⎥ ⎦.
We call s ∈ {-1, 0, 1} u×v the sign matrix, ĉ ∈ R u×v + the coefficient matrix, and e ∈ N v×d the exponent matrix of f . The rows of the exponent matrix are named e 1 ,. . . , e v .

Main Result

Definition 2 (Signed Parametric Systems). A signed parametric system is given by

f = (s • c)x e ,
where the sign matrix s ∈ {-1, 0, 1} u×v and the exponent matrix e ∈ N v×d are specified but the coefficient matrix c is unspecified in the sense that it is left parametric. Formally, c is a u × 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:

⎡ ⎣ f 1 f 2 f 3 ⎤ ⎦ = ⎛ ⎝ ⎡ ⎣ -1 1 -1 0 1 1 1 1 -1 0 1 1 -1 -1 0 ⎤ ⎦ • ⎡ ⎣ 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 ⎤ ⎦ ⎞ ⎠ x 1 x 2 ⎡ ⎢ ⎣ 5 0 2 1 2 0 0 3 0 2 ⎤ ⎥ ⎦
.

This corresponds to

f 1 = -c 11 x 5 1 + c 12 x 2 1 x 2 -c 13 x 2 1 + c 15 x 2 2 f 2 = c 21 x 5 1 + c 22 x 2 1 x 2 + c 23 x 2 1 -c 24 x 3 2 f 3 = c 31 x 5 1 + c 32 x 2 1 x 2 -c 33 x 2 1 -c 34 x 3 2 .
Definition 4 (Parametric Positive Solutions). Consider a signed parametric system f = (s • c)x e . A parametric positive solution of f (x) > 0 is a function z : R u×v + → R d + that maps each possible specification of the coefficient matrix c to a solution of the corresponding non-parametric system, i.e.,

∀ c>0 f z(c) > 0.
Theorem 5 (Main). Let f = (s • c)x e be a signed parametric system. Let

C(n) := i s ik <0 sij >0 (e j -e k )n ≥ 1.
Then the following are equivalent:

(i) f (x) > 0 has a parametric positive solution. (ii) C(n) has a solution n ∈ R d . (iii) C(n) has a solution n ∈ Z d .
In the positive case, the following function z is a parametric positive solution of f (x) > 0:

z(c) = t n , where t = 1 + sij >0 s ik <0 c ik c ij .
In fact, we even have

∀ c>0 ∀ r≥t f (r n ) > 0.
Proof. We first show that (i) implies (ii):

(i) ⇐⇒ ∀ c>0 ∃ x>0 (s • c)x e > 0 ⇐⇒ ∀ c>0 ∃ x>0 i sij >0 c ij x ej > s ik <0 c ik x e k =⇒ ∃ x>0 i sij >0 x ej > s ik <0 2vx e k , by instantiating c =⇒ ∃ x>0 i v max sij >0
x ej > max

s ik <0 2vx e k ⇐⇒ ∃ x>0 i max sij >0
x ej > max

s ik <0 2x e k ⇐⇒ ∃ x>0 i s ik <0 sij >0 x ej > 2x e k ⇐⇒ ∃ x>0 i s ik <0 sij >0 x ej -e k > 2 ⇐⇒ ∃ x>0 i s ik <0 sij >0 (e j -e k ) log 2 x > 1 ⇐⇒ ∃ n∈R d i s ik <0 sij >0
(e je k )n > 1, using log 2 : R + ↔ R =⇒ (ii).

Assume now that (ii) holds. The existence of solutions n ∈ R d and n ∈ Q d of C(n) coincides due to the Linear Tarski Principle: Ordered fields admit quantifier elimination for linear formulas, and therefore Q is an elementary substructure of R with respect to linear sentences [START_REF] Loos | Applying linear quantifier elimination[END_REF]. Given a solution n ∈ Q d , we can use the principal denominator δ ≥ 1 of all coordinates of n to obtain a solution δn ∈ Z d . Hence (iii) holds.

We finally show that (iii) implies (i):

(i) ⇐⇒ ∀ c>0 ∃ x>0 (s • c)x e > 0 ⇐⇒ ∀ c>0 ∃ x>0 i sij >0 c ij x ej > s ik <0 c ik x e k ⇐= ∀ c>0 ∃ x>0 i max sij >0 c ij x ej > s ik <0 c ik max s ik <0 x e k ⇐⇒ ∀ c>0 ∃ x>0 i s ik <0 sij >0 c ij x ej > s ik <0 c ik x e k ⇐⇒ ∀ c>0 ∃ x>0 i s ik <0 sij >0 x ej -e k > s ik <0 c ik c ij ⇐= ∀ c>0 ∃ x>0 i s ik <0 sij >0
x ej -e k ≥ t, where t = 1 +

s i j >0 s i k <0 c i k c i j ⇐⇒ ∀ c>0 ∃ x>0 i s ik <0 sij >0 (e j -e k ) log t x ≥ 1 ⇐⇒ ∃ n i s ik <0 sij >0
(e je k )n ≥ 1, using log t : R + ↔ R ⇐= ∃

n∈Z d i s ik <0 sij >0 (e j -e k )n ≥ 1 ⇐⇒ (iii).
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 ≥ t would work there as well.

Example 6. Consider f1 f2 with f 1 , f 2 taken from Example 3:

f 1 = -c 11 x 5 1 + c 12 x 2 1 x 2 -c 13 x 2 1 + c 15 x 2 2 f 2 = c 21 x 5 1 + c 22 x 2 1 x 2 + c 23 x 2 1 -c 24 x 3 2 .

This gives us

s = -1 1 -1 0 1 1 1 1 -1 0 and e = ⎡ ⎢ ⎢ ⎢ ⎢ ⎣ 5 0 2 1 2 0 0 3 0 2 ⎤ ⎥ ⎥ ⎥ ⎥ ⎦
. We obtain C(n) as follows:

2 1 -5 0 n ≥ 1 ∨ 0 2 -5 0 n ≥ 1 ∧ 2 1 -2 0 n ≥ 1 ∨ 0 2 -2 0 n ≥ 1 ∧ 5 0 -0 3 n ≥ 1 ∨ 2 1 -0 3 n ≥ 1 ∨ 2 0 -0 3 n ≥ 1 , which simplifies to ( -3 1 n ≥ 1 ∨ -5 2 n ≥ 1) ∧ ( 0 1 n ≥ 1 ∨ -2 2 n ≥ 1) ∧ ( 5 -3 n ≥ 1 ∨ 2 -2 n ≥ 1 ∨ 2 -3 n ≥ 1).
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 [START_REF] Barrett | CVC4[END_REF], MathSat [START_REF] Cimatti | The MathSAT5 SMT solver[END_REF], SMT-RAT [START_REF] Corzilius | SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving[END_REF], Yices [START_REF] Dutertre | Yices 2.2[END_REF], or Z3 [START_REF] De Moura | Z3: an efficient SMT solver[END_REF]. All these tools certify satisfiability and give a possible solution for n, which is called a model in the SMT world:

n = -5 2 -2 .
Hence (s • c)x e > 0 has a parametric positive solution, e.g.,

z(c) = t -5 2 t -
f 1 = -c 11 x 5 1 + c 12 x 2 1 x 2 -c 13 x 2 1 + c 15 x 2 2 f 3 = c 31 x 5 1 + c 32 x 2 1 x 2 -c 33 x 2 1 -c 34 x 3 2 .
That is

s = -1 1 -1 0 1 1 1 -1 -1 0 , e = ⎡ ⎢ ⎢ ⎢ ⎢ ⎣ 5 0 2 1 2 0 0 3 0 2 ⎤ ⎥ ⎥ ⎥ ⎥ ⎦ .
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 ∈ R 2 . Hence (s • c)x e > 0, i.e. f 1 > 0, f 3 > 0, does not have a parametric positive solution.

Nevertheless, with the concrete instantiations f1 , f3 from Example 1 the corresponding system f1 > 0, f3 > 0 of inequalities is feasible in R 2 + . One possible solution is

3 2 3 2
. However, if we change the absolute value of the leading coefficient of f1 from 1 to 4 yielding f * 2 illustrates the situation.

1 = -4x 5 1 + 4x 2 1 x 2 -2x 2 1 + x 2 2 , then f * 1 > 0, f3 > 0 is infeasible in R 2 + . Figure

A Re-analysis of Subtropical Methods

For non-parametric systems of real polynomial inequalities, heuristic Newton polytope-based subtropical methods [START_REF] Fontaine | Subtropical satisfiability[END_REF][START_REF] Sturm | Subtropical real root finding[END_REF] 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 • 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 [START_REF] Errami | Detection of Hopf bifurcations in chemical reaction networks using convex coordinates[END_REF].

In the second area, a subtropical approach for systems of several polynomial inequalities has been integrated with the SMT solver veriT [START_REF] Bouton | veriT: an open, trustable and efficient SMT-solver[END_REF]. 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 [START_REF] Fontaine | Subtropical satisfiability[END_REF].

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.

Subtropical Real Root Finding

In [START_REF] Sturm | Subtropical real root finding[END_REF] we have studied an incomplete method for heuristically finding a positive solution for a single multivariate polynomial inequality with fixed integer coefficients:

[ f1 ] = (s • ĉ)x e where s ∈ {-1, 0, 1} 1×v , ĉ ∈ Z 1×v + , e ∈ N v×d .
The method considers the positive and the negative support, which in terms of our notions is given by

S + = { e j | s 1j > 0 }, S -= { e k | s 1k < 0 }.
Then [37, Lemma 4] essentially states that f 1 (x) > 0 has a positive solution if

C := ej ∈S + ∃ n∈R d ∃ γ∈R ⎛ ⎜ ⎜ ⎝ -e j 1 n γ ≤ -1 ∧ e k ∈S + ∪S - e k =ej e k -1 n γ ≤ -1 ⎞ ⎟ ⎟ ⎠ .
Unfortunately, in [START_REF] Sturm | Subtropical real root finding[END_REF]Lemma 4] vectors e l = 0 • • • 0 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 [START_REF] Fontaine | Subtropical satisfiability[END_REF]Lemma 2].

The proof of the loop invariant (I 1 ) in [37, Theorem 5(ii)] shows that the positive support need not be considered in the conjunction:

C ⇐⇒ ej ∈S + ∃ n∈R d ∃ γ∈R ⎛ ⎝ -e j 1 n γ ≤ 1 ∧ e k ∈S - e k -1 n γ ≤ -1 ⎞ ⎠ .
Starting with Fourier-Motzkin elimination [34, Sect. 12.2] of γ, we obtain

C ⇐⇒ ej ∈S + ∃ n∈R d e k ∈S - (e k -e j )n ≤ -2 ⇐⇒ ej ∈S + ∃ n∈R d e k ∈S - (e j -e k )n ≥ 1 ⇐⇒ ∃ n∈R d ej ∈S + e k ∈S - (e j -e k )n ≥ 1 ⇐⇒ ∃ n∈R d max ej ∈S + (e j n) ≥ max e k ∈S - (e k n + 1) ⇐⇒ ∃ n∈R d e k ∈S -ej ∈S + (e j -e k )n ≥ 1 ⇐⇒ ∃ n∈R d C(n),
with C(n) as in Theorem 5.

Corollary 8. Let f ∈ Z[x 1 , . . . , x d ], say, f = (s • ĉ)x e , where s ∈ {-1, 0, 1} 1×v , ĉ ∈ Z 1×v + , e ∈ N v×d . Let f = (s • c)x e
, where c is a 1 × v-matrix of pairwise different indeterminates. Then the following are equivalent:

(i) The algorithm find-positive [37, Algorithm 1] does not fail, and thus finds a rational solution of f > 0 with positive coordinates. (ii) There is a row e j of e with s 1j > 0 such that the following LP problem has a solution n ∈ Q d :

s 1k <0
(e je k )n ≥ 1.

(iii) f > 0 has a parametric positive solution.

In the positive case, f (r n ) > 0 for all r ≥ 1 + v s 1k <0 ĉ1k .

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

According to Theorem 5, a solution for f > 0 can be obtained by plugging ĉ 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.

t = 1 + s1j >0 s 1k <0 ĉ1k ĉ1j ≤ 1 + s1j >0 s 1k <0 ĉ1k 1 ≤ 1 + v s 1k <0
ĉ1k .

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 [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF] 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.

Subtropical Satisfiability Checking

Subsequent work [START_REF] Fontaine | Subtropical satisfiability[END_REF] takes an entirely geometric approach to generalize the work in [START_REF] Sturm | Subtropical real root finding[END_REF] from one polynomial inequality to finitely many such inequalities. Consider a system with fixed integer coefficients in our notation:

f = ⎡ ⎢ ⎣ f1 . . . fu ⎤ ⎥ ⎦ = (s • ĉ)x e , where s ∈ {-1, 0, 1} u×v , ĉ ∈ Z u×v + , e ∈ N v×d .
Then [START_REF] Fontaine | Subtropical satisfiability[END_REF]Theorem 12] derives essentially the following sufficient condition for the existence of a positive solution of f > 0:

C := ∃ n∈R d ∃ γ1∈R . . . ∃ γu∈R u i=1 ⎛ ⎝ ⎛ ⎝ sij >0 e j n + γ i > 0 ⎞ ⎠ ∧ s ik <0 e k n + γ i < 0 ⎞ ⎠ .
After an equivalence transformation, we can once more apply Fourier-Motzkin elimination [34, Sect. 12.2]:

C ⇐⇒ ∃ n∈R d u i=1 sij >0 ∃ γi∈R e j n + γ i > 0 ∧ s ik <0 e k n + γ i < 0 ⇐⇒ ∃ n∈R d u i=1 sij >0 s ik <0 (e j -e k )n > 0 ⇐⇒ ∃ n∈R d u i=1 max sij >0 e j n > max s ik <0 e k n ⇐⇒ ∃ n∈R d u i=1 s ik <0 sij >0 (e j -e k )n > 0 ⇐⇒ ∃ n∈R d u i=1 s ik <0 sij >0 (e j -e k )n ≥ 1 ⇐⇒ ∃ n∈R d C(n),
with C(n) as in Theorem 5.

Corollary 9. Let f ∈ Z[x 1 , . . . , x d ] u , say, f = (s•ĉ)x e , where s ∈ {-1, 0, 1} u×v , ĉ ∈ Z u×v + , e ∈ N v×d . Let f = (s • c)x e
, where c is a u × v-matrix of pairwise different indeterminates. Then the following are equivalent:

(i) The incomplete subtropical satisfiability checking method for several inequalities over QF NRA (quantifier-free nonlinear real arithmetic) introduced in [START_REF] Fontaine | Subtropical satisfiability[END_REF] succeeds on f > 0. (ii) The following SMT problem with unknowns n is satisfiable over QF LRA (quantifier-free linear real arithmetic):

u i=1 s ik <0 sij >0
(e je k )n ≥ 1.

(iii) f > 0 has a parametric positive solution.

In the positive case, f (r n ) > 0 for all r ≥ 1 + v

s ik <0
ĉik .

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

The equivalence between (i) and (iii) in the corollary states the following: The procedure in [START_REF] Fontaine | Subtropical satisfiability[END_REF] 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 [START_REF] Fontaine | Subtropical satisfiability[END_REF], the work has been implemented within a combination of the veriT solver [START_REF] Bouton | veriT: an open, trustable and efficient SMT-solver[END_REF] with the library STROPSAT [START_REF] Fontaine | Subtropical satisfiability[END_REF]. 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 [START_REF] Fontaine | Subtropical satisfiability[END_REF] 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 ι and κ be the numbers of positive and negative coefficients, respectively. Then compared to [START_REF] Fontaine | Subtropical satisfiability[END_REF] we have reduced d + u variables to d variables, and we have reduced uκ clauses with ι atoms each plus u unit clauses to some different uκ clauses with ι 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 [START_REF] Fontaine | Subtropical satisfiability[END_REF] 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 [START_REF] Sturm | Subtropical real root finding[END_REF]Algorithm 1,.

Fig. 1 .

 1 Fig. 1. An SMT-LIB input file for Example 6

Fig. 2

 2 Fig. 2 illustrates the situation.

Fig. 2 .

 2 Fig. 2. Implicit plots of varieties of polynomials from Examples 6 and 7. (a) Both polynomials are positive in the region containing (0.0003, 0.0015). Since this point is an instance of a parametric positive solution, there will be a suitable point under all modifications of absolute values of coefficients of the polynomials. (b) Both polynomials are positive in the region containing (1.5, 1.5). (c) After modifying the absolute value of the leading coefficient of f1 the polynomials are not simultaneously positive in the first quadrant anymore. Example 7. We slightly modify Example 6 and consider the subsystem f1 f3 of Example 3:

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.


Sébastien Rimbert
email: sebastien.rimbert@inria.fr

Nathalie Gayraud

Maureen Clerc

Stéphanie Fleck

Laurent Bougrain

Can the MIQ-RS questionnaire be used to estimate the performance of a MI-based BCI?

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction:

Predicting a subject's ability to use the interface with good accuracy is one of the major issues in the motor Brain-Computer interface (BCI) domain. A few recent studies show that subjective questionnaires could be used to predict the performance of motor imagery (MI) based BCI. Indeed, the Kinesthetic and Visual Imagery Questionnaire (KVIQ), could allow a better predictability of BCI-illiterate cases [START_REF] Vuckovic | Using a motor imagery questionnaire to estimate the performance of a Brain-Computer Interface based on object oriented motor imagery[END_REF]. Another more recent questionnaire called the Motor Imagery Questionnaire Revised-Second Edition (MIQ-RS) is a suitable option for examining MI ability [START_REF] Butler | The Movement Imagery Questionnaire-Revised, Second Edition (MIQ-RS) Is a Reliable and Valid Tool for Evaluating Motor Imagery in Stroke Populations[END_REF]. In 2016, Marchesotti et al. found that the representation of subjective behaviour, calculated using the MIQ-RS questionnaire, and the control of the BCI were intimately linked [START_REF] Marchesotti | Quantifying the role of motor imagery in brain-machine interfaces[END_REF]. However, in these studies [START_REF] Vuckovic | Using a motor imagery questionnaire to estimate the performance of a Brain-Computer Interface based on object oriented motor imagery[END_REF][START_REF] Marchesotti | Quantifying the role of motor imagery in brain-machine interfaces[END_REF], the performance of the classifier was calculated for a right-hand MI versus a left-hand MI task. In this abstract, we classify between resting state and imagined movement, which is a relevant classification task in BCI research [START_REF] Townsend | Continuous EEG classification during motor imagery-simulation of an asynchronous BCI[END_REF]. The aim of this study is to answer the following question for a resting state versus MI classification task: can the MIQ-RS be used to estimate the performance of an MIbased BCI?

Material, Methods and Results: 36 right-handed healthy subjects (12 females; aged 31.3 years ± 14.4) were tested for their perception level of their visual and kinesthetic MI ability via the MIQ-RS questionnaire. EEG signals were recorded with a Biosemi Active Two 32-channel EEG system during a MI task (i.e. a single closing of the right hand) in one session of 40 trials. The EEG signal was bandpassed using a Butterworth filter between 8 and 30 Hz and segmented into 3.5 second trials. A Riemannian-based Tangent Space classification method [START_REF] Barachant | Riemannian geometry applied to BCI classification[END_REF] coupled with a Logistic Regression classifier was used to generate classification results in a 4-fold cross validation scheme. We computed the correlation between the classification results and both the kinesthetic (K) and the visual scores (V). The recovered Pearson correlation coefficient was equal to ρ = 0.02, (p-value = 0.87) in the first comparison, and ρ = -0.12 (p-value = 0.47) in the second. Moreover, we performed a Principal Component Analysis over the aforementioned three features (Figure 1A) whose analysis produced no indication of any correlation between them. Finally, we observed 3 different profiles according to users' MIQ-RS values (identified K+ and/or V+ if their score is over 70%, K-and/or V-otherwise). We computed the average accuracy of each class (Figure 1B) and performed Welch's t-test to verify the statistical significance of the differences between the average classification results. We obtained the following p-values: 0.118 between K+V+ and K-V+; 0.714 between K+V+ and K-V-; and 0.048 between K-V-and K-V+. Finally, we computed the Event-Related Spectral Perturbation (ERSP) between 5-30 Hz within each group using the EEGlab toolbox and we again compared the differences between groups. The obtained p-values were all superior to 0.01.

Discussion:

Our results revealed no correlation between the classification results and the MIQ-RS scores, contrary to those suggested by [START_REF] Vuckovic | Using a motor imagery questionnaire to estimate the performance of a Brain-Computer Interface based on object oriented motor imagery[END_REF][START_REF] Marchesotti | Quantifying the role of motor imagery in brain-machine interfaces[END_REF]. While the classification results and ERSPs differ upon grouping the subjects according to their MIQ-RS profiles, we found no statistical significance (at p-value < 0.01).

Significance:

Our results demonstrate that the MIQ-RS questionnaire cannot be used to estimate the performance of a MI-BCI based on distinguishing between resting state and right-hand MI tasks.

Figure 1 :

 1 Figure 1: (A) Principal Component Analysis performed over 36 right-handed healthy subjects for the classification accuracy, the kinesthetic subscale and the visual subscale. The explained variance ratio of each component is 41%, 34% and 25% (B) Kinesthetic scale, visual scale, accuracy and number of subjects according to MIQ-RS profile (K+V+ in red; K-V-in blue; K-V+ in green).