A Combined VTS/Lazard Quantifier Elimination Method

Abstract

Many nonlinear optimisation problems involving systems of multivariate polynomial constraints can be expressed as Quantifier Elimination problems. In this regard, the need to eliminate quantifiers presents itself in many real problems such as in economics, mechanics, and motion planning. We focus on using Cylindrical Algebraic Decomposition and Virtual Term Substitution simultaneously. In this paper, we introduce the state-of-the-art theory behind an implementation of these methods produced in collaboration with Maplesoft .

Keywords

• eol>Quantifier Elimination
• Cylindrical Algebraic Decomposition
• Virtual Term Substitution
• Equational Constraints

1. Introduction

Quantifier Elimination (QE) over the real numbers refers to problems in Computer Algebra of producing a quantifier-free equivalent representation of a logical expression defined by polynomial constraints. Quantifier Elimination is highly relevant and necessary for many applications from diferent fields of study. Nonlinear optimisation problems and conditions on solvability and satisfiability of systems of multivariate polynomial equations and inequalities can canonically be presented as QE problems. QE problems are known to arise in economics [1, 2], mechanics [3], mathematical biology [4, 5, 6], reaction networks [7], AI to pass mathematical exams [8], and motion planning [9].

In this paper, we introduce the theoretic background that is inside the QE implementation of the second author as a part of his Ph.D. studies under the guidance of the first author [ 10]. This Maple implementation, the package QuantifierElimination, is now being integrated to the main program by the second author and it will be available to all Maple users without the need of downloading and installing a third party package. One main aim of this implementation is to mitigate the high running times of QE problems by avoiding unnecessary and/or complex computations by using a poly-algorithmic approach to QE to pick the route of expected least resistance. Moreover, the poly-algorithm ofers full incrementality as a whole. Interested readers can find more about the implementation and its design decisions in [ 10, 11]. In particular [10, §7.4] has the benchmarking data.

2. Definitions

A logical formula of integral multivariate polynomial constraints, (1, . . . , ) 0 for some ∈ N and ∈ {=, ̸=, >, ≥ , <, ≤} , joined together with logical connectives ∧, and ∨ is called a Tarski formula. A single polynomial constraint in a Tarski formula is called an atom. Finally, the language of all semi-algebraic propositions is called a Tarski-language.

Given a Tarski formula (1, . . . , ), and a list of quantifiers on 1, . . . , for some integer 1 ≤ ≤ . A (prenex) quantified Tarski formula is 11 22 . . . (1, . . . , , . . . , ), ( 1 ) where = ∀ or ∃. The QE problem is then two-fold: Is there a quantifier-free Tarski formula (+1, . . . , ) equivalent to ( 1 )? And, if so, can it be computed?

In 1951, Tarski showed that the real quantifier elimination problem is decidable for Tarski formulas involving multivariate polynomials with rational coeficients. Moreover, he gave an algorithm (insuperable complexity) to calculate the equivalent quantifier-free formula.

Collins [12] produced a QE algorithm through calculating a sign-invariant Cylindrical Algebraic Decomposition (CAD) in 1975, and proved that, starting with a Tarski formula with degree polynomials in variables, CAD computations have doubly exponential complexity: ˆ2ˆ(2 + ( 1 )). This is due to the need of squaring the degree of the polynomials and their number at each one of the variable elimination steps. McCallum [13] showed that, under some assumptions that certain polynomials don’t vanish on some varieties, the doubly exponential complexity of calculating a order-invariant CAD of a given Tarski formula can be lowered to ˆ2ˆ( + ( 1 )). In 1994, Lazard [14] suggested a new procedure for projecting and lifting for lex-least invariant CAD calculations that steers clear of the assumptions needed in McCallum’s procedure, and in [15], McCallum–Parusiński–Paunescu justified the correctness of Lazard’s procedure, and the same ˆ2ˆ( + ( 1 )) complexity. The rfist author and Heintz [ 16] have shown that doubly-exponential complexity is intrinsic to quantifier elimination, admittedly with a double exponent lower bound of /5 + ( 1 ), later improved to /3 + ( 1 ) by [17].

We should also note that the degrees of the polynomials and the number of polynomials in a Tarski formula are not the only sources of the doubly exponential complexity of quantifier elimination. Given a quantified Tarski formula, let be the number of alterations of quantifiers. For example, = 3 if we have the quantifiers in the ∀∀∃∀∃∃∃ order. Brown and the first author [17] have provided an example involving only linear polynomials that manifests a doubly exponential behaviour in , caused (in the case of VTS) by the repeated conversion between conjunctive and disjunctive normal form forced by the alternations: see the remark at the start of §4.

Starting from a diferent origin, Weispfenning introduced the technique of Virtual Term Substitution (VTS) for purely existential QE problems for linear [18], quadratic [19] and cubic [20] polynomials. Later in his doctoral studies Košta [21] wrote down explicit algorithms for VTS for all degrees ≤ 3. 3. Quantifier Elimination by Projection and Lifting This was originated in [12]. An improvement, but which could occasionally deliver a result lfagged as “potentially incomplete”, was in [ 13]. A solution was suggested by Lazard in [14], but only proved in [15]. It uses lexicographically-least (lex-least) invariance rather than McCallum’s order-invariance. The projection phases of both approaches are similar. A development, skipping trailing coeficients in projection in many cases, was introduced in [22]. 3.1. Lazard Projection and Lifting The lex-least invariance means that we require polynomials to have a certain expansion on varieties. For a given multivariate polynomial (1, . . . , ) and a point a = (1, . . . , ), we want the lex-least monomial of to have the expansion a(1 − 1) 1 (2 − 2) 2 . . . ( − ) , ( 2 ) where a is a non-zero integer and s are non-negative integers. This selection creates a big diference in the lifting phase. If becomes zero for a trail of variable assignments a, i.e. vanishes on some variety that a is in, the McCallum procedure would need to come to a halt. On the other hand, for Lazard lifting, one can use the lex-least invariance and replace with a divided by ( 2 ). The outcome polynomial still has integer coeficients and it is in the Tarski language. It is easy to see that the outcome polynomial is non-zero at a and one can proceed with the lifting procedure.

The guaranteed lex-least factorisation and replacing a nullified polynomial by its zero-free part is a clear advantage of Lazard lifting. However, this should not create a false image. There are still cases where nullification of polynomials are a problem, especially when we have equational constraints (§3.2) in the Tarski formulae. More on these special cases and relevant research can be found in [23, 24].

Most projection-lifting1 CAD implementations available to the public today use McCallum’s projection and lifting procedure to calculate CADs. To the best of our knowledge, the second author’s implementation is the first QE implementation that uses Lazard’s procedure in CAD calculations. This is certainly true for an implementation made in the Maple language. 3.2. Equational Constraints In this section we assume that we start with a Tarski formula made up of polynomial constraints where exactly of these constraints are equations: 1 = 0 ∧ 2 = 0 ∧ = 0 ∧ 1 10 ∧ 2 20 ∧ · · · ∧ − − 0, ( 3 ) where all of the polynomials are from the polynomial ring Z[1, . . . , ] and ∈ {̸=, <, ≤ , > , ≥} . The atoms in the Tarski formula with the equations are called equational constraints.

Collins [26] raised the question of whether an single equational constraint ( = 1 in ( 3 )) in a Tarski formula be used to our advantage in CAD calculations. In 1999 for = 1 case and in 2001 1As opposed to, say, Regular Chains approaches [25]. for general , McCallum [27, 28] showed that the presence of equational constraints reduces the double exponential complexity ˆ2ˆ( + ( 1 )) drastically to ˆ2ˆ( − + ( 1 )).

We would also like to note that more improvements and extensions has been made on treating equational constraints. The first author in collaboration with others [ 29] generalised the use of equational constraints when only a part of the formula has equational constraints. In 2020, it was shown that Gröbner bases can be used rather than just using iterated resultants [30] and that this approach reduces the polynomial degree growth. Generically, this lowers the doubly exponential complexity in the polynomial degrees to ˆ2ˆ( − + ( 1 )).

These results make a clear case for their benefit. In essence the equational constraint treatment reduces the doubly exponential complexity of CAD calculations significantly by removing the number of such equalities from the Tarski formula. It should still be noted that all these mentioned results are for the McCallum projection and lifting procedure and they require well-orientedness assumptions.

The second author’s implementation, on the other hand, uses the Lazard’s procedure and therefore cannot yet enjoy all the simplifications that equational constraints have to ofer. The research on equational constraints while using Lazard’s approach is at its early stages. At the time of implementation, by the Ph.D. work of Nair [24] we only knew how to process a single equational constraint in Lazard-based CAD computations (this has now been extended). Moreover, we require the polynomial in the equational constraint to satisfy some non-vanishing properties on varieties. The QE implementation of the second author handles Tarski formulae with a single equational constraint, and it has the capabilities to notice whether this equational constraints satisfies the assumptions necessary coming from Nair’s conditions. Moreover, the QuantifierElimination package implements bespoke routines Nair outlined [24] for the recovery of problematic cases once such a problem is identified. On top of it all, this software takes full advantage of the avoidance and recovery of the problematic cases by employing Collins and Hong’s partial CAD [31] construction.

4. Virtual Term Substitution (VTS)

Virtual Term Substitution (VTS) is a method with geometric roots to handle QE problems where the Tarski formulae are purely existentially quantified: see [ 18]. One can still apply VTS to a universally quantified problem by logically negating the QE problem first: ∀ () ≡ ¬∃¬ (). This is a step that can give rise to complexity growth: ∃¬ () is a disjunction over all the guards (see ( 4 )), which will be turned by ¬ into a conjunction, and conversion to disjunctive normal form can cause exponential blowup.

Consider an existentially quantified Tarski formula ∃ (u, ), where explicit negations in have been eliminated by De Morgan’s Laws.. The aim of VTS is to compute a finite list of conditions (called guards) and relative virtual substitution points for the existentially quantified variable so that QE can be performed by turning the problem replacing under the conditions of the guards. More precisely, VTS tries to split the -axis into all relevant intervals and tries to identify a finite set = {( , )} of pairs where are guard conditions and are sample points from each interval on the real axis. Under these conditions we can see the following Definition 1 (Virtual Substitution). [21, Section 2.3] The virtual substitution of a structural test point (u) for into a quantifier free relation (u, ) 0 is (u) := [// ] a quantifier free formula such that for any parameter values a ∈ R− 1, if a satisfies the guard of , then a satisfies if and only if (a, (a)) 0 is true. (a) is well-defined because the guard is satisfied. In addition, we have to deal with virtually substituting ±∞ : see [21, p. 36]. 4.1. Example We would like to exemplify this idea on a simple case with a single existential quantifier. Assume that we start with the simple quantified Tarski formula

∃ ( − = 0 ∧ + > 0) .

Naïvely, one can solve this QE problem by algebraically (and carelessly) solving the first atom of the Tarski formula as = / (to be our virtual substitution point) and by plugging this value in the second atom:

(/) + > 0.

This simple approach ignores many possibilities that requires attention. As it is given, ( 6 ) is only meaningful under the guard that ̸= 0. Furthermore, the Tarski language does not include rational values therefore clearing any denominators is necessary. Even at this step one needs to consider that is either negative or positive, therefore clearing denominators might change the inequality. We can instead clear the denominators by multiplying each side of ( 6 ) with 2 to keep the constraint unchanged. These considerations give us one of the right-hand sides cases in ( 4 ) as

( ̸= 0 ∧ + 2 > 0).

Remark that ( 7 ) is not equivalent to ( 5 ). For that one also needs other conditions such as correspondence ∃ (u, ) ⇔

⋁︁ ( ,)∈

( ∧ (u, //)) .

( = 0 ∧ = 0 ∧ ̸= 0) ∨ ( = 0 ∧ = 0 ∧ = 0 ∧ > 0).

The Tarski formulae ( 7 ) and ( 8 ) put together with disjunction is logically equivalent to ( 5 ) and it is free of the quantified variable . 4.2. VTS in general It is easy to see that once the VTS points are established, an ∃ quantifier is eliminated by moving from the problem on the left-hand side of ( 4 ) to the right-hand side. Having said that, it is not always possible to identify the set . Weispfenning [18, 19] gave us for the linear and quadratic cases, and [20] outlined the cubic case.

Including Košta’s [21] detailed algorithms for cubic VTS and the corrections in Appendix A, this method is implemented in second author’s QE package. This QE implementation is believed to be the first in Maple, and certainly the first in Maple to include the degree 3 VTS algorithms. ( 4 ) ( 5 ) ( 6 ) ( 7 ) ( 8 ) 4.3. Degree Growth in VTS Although at the start all the variables in the Tarski formula ( 5 ) appeared linearly, after the suggested virtual substitution and simplification ( 7 ), we saw that the degree of variable increased. This hints shows successive runs of VTS might afect the applicability of VTS since this method requires the degrees of the variables to be ≤ 3. For example, let’s start with the quantified Tarski formula

∃∃ (︀ 3 − = 0 ∧ + > 0)︀ similar to ( 5 ). The application of VTS to the variable , as it was done for ( 5 ), yields ∃ (︀ (3 ̸= 0 ∧ 3 + 6 > 0) ∨ (3 = 0 ∧ = 0 ∧ ̸= 0)

∨(3 = 0 ∧ = 0 ∧ = 0 ∧ > 0))︀ .

The degree of the variable in the first Tarski formula of ( 10 ) is 6. Therefore, without a change of variables, VTS can no longer be employed for elimination of the existential quantifier on . Such a problem can be avoided by a better variable ordering. We look at the following Tarski formula:

∃∃ (︀ 3 − = 0 ∧ + > 0)︀ , which is equivalent to ( 9 ). After applying VTS for variable , we get

∃ (( ̸= 0 ∧ + > 0) ∨ ( = 0 ∧ = 0 ∧ + > 0)) .

This time it is possible to apply VTS to all parts of ( 10 ) to eliminate the quantifier on (as this variable appears with degree ≤ 3 in the output). Hence, we see that the variable ordering can have an efect on the applicability of VTS. This is a characteristic diference between VTS and CAD; in CAD, the order of variables can afect the running time heavily but the variable ordering never renders this method inapplicable.

5. Conclusion and Future Directions

The poly-algorithmic QE implementation is a promising tool that is at its early stages. With its various variable ordering strategies and QE methods it already is a sophisticated system that ofers Maple users a lot of options. Moreover, any research done, especially on Lazard’s CAD construction procedure, would directly benefit this implementation. For that, it is of interest to us to compare and understand the strengths of McCallum and Lazard’s procedures against each other and to find ways to identify the situations where these approaches fail to yield answers. It is also a top priority to develop theory around equational constraints using Lazard’s projection/lifting that is analogous to the theory already developed around McCallum’s procedure.

Neither the guards nor the virtual sample points are unique; we are optimistic that a diferent splitting of a given problem (such as ( 5 )) can help to keep the variable degrees low. Not only that, similar to the CAD case, the variable ordering in VTS can be relevant when the QE problem has multiple existential constraints in a block (see §4.3). More experiments on diferent guard selections and variable orderings are needed to make full use of virtual term substitutions. ( 9 ) ( 10 ) ( 11 ) ( 12 )

6. Acknowledgement

The authors are grateful to Marek Košta and Jürgen Gerhard for correspondence about Appendix A. The first author would like to thank the EPSRC grant number EP/T015713/1 for supporting his research. The second author would like to thank EPSRC and Maplesoft for funding his research studentship. The third author would like to thank the EPSRC grant number EP/T015713/1 and the FWF grant P-34501N for partially supporting his research. C. Bajaj (Ed.), Proceedings Algebraic Geometry and its Applications: Collections of Papers from Shreeram S. Abhyankar’s 60th Birthday Conference, 1994, pp. 467–476. [15] S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard’s method for CAD construction, J. Symbolic Comp. 92 (2019) 52–69. [16] J. Davenport, J. Heintz, Real Quantifier Elimination is Doubly Exponential, J. Symbolic

Comp. 5 (1988) 29–35. [17] C. Brown, J. Davenport, The Complexity of Quantifier Elimination and Cylindrical Algebraic Decomposition, in: C. Brown (Ed.), Proceedings ISSAC 2007, 2007, pp. 54–60. [18] V. Weispfenning, The Complexity of Linear Problems in Fields, J. Symbolic Comp. 5 (1988) 3–27. [19] V. Weispfenning, Quantifier elimination for real algebra — the quadratic case and beyond,

AAECC 8 (1997) 85–101. [20] V. Weispfenning, Quantifier elimination for real algebra — the cubic case, in: Proceedings

ISSAC 1994, 1994, pp. 258–263. [21] M. Košta, New concepts for real quantifier elimination by virtual substitution, Ph.D. thesis,

Universität des Saarlandes, 2016. [22] C. Brown, S. McCallum, Enhancements to Lazard’s Method for Cylindrical Algebraic Decomposition, in: F. Boulier, M. England, T. Sadykov, E. Vorozhtsov (Eds.), Computer Algebra in Scientific Computing CASC 2020, volume 12291 of Springer Lecture Notes in Computer Science, 2020, pp. 129–149. doi:https://doi.org/10.1007/978-3-030-60026-6_8. [23] A. Nair, J. Davenport, G. Sankaran, Curtains in CAD: Why Are They a Problem and How Do We Fix Them?, in: A. Bigatti, J. Carette, J. Davenport, M. Joswig, T. de Wolf (Eds.), Mathematical Software — ICMS 2020, volume 12097 of Springer Lecture Notes in Computer Science, Springer, 2020, pp. 17–26. [24] A. Nair, Curtains in Cylindrical Algebraic Decomposition, Ph.D. thesis, University of Bath, 2021. URL: https://researchportal.bath.ac.uk/en/studentTheses/ curtains-in-cylindrical-algebraic-decomposition. [25] R. Bradford, C. Chen, J. Davenport, M. England, M. Moreno Maza, D. Wilson, Truth Table Invariant Cylindrical Algebraic Decomposition by Regular Chains, in: Proceedings CASC 2014, 2014, pp. 44–58. [26] G. Collins, Quantifier elimination by cylindrical algebraic decomposition — twenty years of progess, in: B. Caviness, J. Johnson (Eds.), Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer Verlag, Wien, 1998, pp. 8–23. [27] S. McCallum, On Projection in CAD-Based Quantifier Elimination with Equational Constraints, in: S. Dooley (Ed.), Proceedings ISSAC ’99, 1999, pp. 145–149. [28] S. McCallum, On Propagation of Equational Constraints in CAD-Based Quantifier Elimination, in: B. Mourrain (Ed.), Proceedings ISSAC 2001, 2001, pp. 223–230. [29] R. Bradford, J. Davenport, M. England, S. McCallum, D. Wilson, Truth table invariant cylindrical algebraic decomposition, J. Symbolic Comp. 76 (2016) 1–35. [30] M. England, R. Bradford, J. Davenport, Cylindrical Algebraic Decomposition with Equational Constraints, in: J. Davenport, M. England, A. Griggio, T. Sturm, C. Tinelli (Eds.), Symbolic Computation and Satisfiability Checking: special issue of J. Symbolic Computation, volume 100, 2020, pp. 38–71. [31] G. Collins, H. Hong, Partial Cylindrical Algebraic Decomposition for Quantifier Elimina

A. Correction to [21]

There is a correction necessary with respect to [21, p. 58]. The setting is that is a cubic, with a root defined by and an index . We wish to investigate (), where is linear or quadratic in (the highest degrees necessary when is defined by a cubic). Let * be ≤ if is <, and < if is ≤ .

Step 3.1 the value assigned to − should be ¬(− * 0)[//(, )] in the cases is not =. Step 4 has a typo: instead of ∈ {=, <, ≤}

it should be ∈ {̸=, >, ≥} .

Step 4.1 An analogous change to 3.1, but the way the code in [10] is written, this case is never reached, provided that the ̸= 0 case is handled separately.

References

[1] C. Mulligan , R. Bradford , J. Davenport , M. England , Z. Tonks , Quantifier Elimination for Reasoning in Economics , https://arxiv.org/abs/ 1804 .10037, 2018 .

[2] C. Mulligan , J. Davenport , M. England, TheoryGuru: A Mathematica Package to Apply Quantifier Elimination Technology to Economics , in: J. Davenport , M. Kauers , G. Labahn, J. Urban (Eds.), Proceedings Mathematical Software - ICMS 2018 , 2018 , pp. 369 - 378 .

[3] N. Ioakimidis , Sharp bounds based on quantifier elimination in truss and other applied mechanics problems with uncertain, interval forces/loads and other parameters , Technical Report TR-2019-Q7 University of Patras, 2019 .

[4] C. Brown , M. El Kahoui , D. Novotni , A. Weber , Algorithmic methods for investigating equilibria in epidemic modeling , J. Symbolic Comp . 41 ( 2006 ) 1157 - 1173 .

[5] G. Röst , A. Sadeghimanesh , Exotic Bifurcations in Three Connected Populations with Allee Efect , International Journal of Bifurcation and Chaos Issue 13 art. no. A36 31 ( 2021 ).

[6] C. Chauvin , M. Müller , A. Weber , An application of quantifier elimination to mathematical biology , In Computer Algebra in Science and Engineering (Fleischer ( 1995 ) 287 - 296 .

[7] H. Rahkooy , T. Sturm, Parametric Toricity of Steady State Varieties of Reaction Networks , in: Proceedings CASC 2021: Computer Algebra in Scientific Computing , 2021 , pp. 314 - 333 .

[8] Y. Wada , T. Matsuzaki , A. Terui , N. Arai , An Automated Deduction and Its Implementation for Solving Problem of Sequence at University Entrance Examination, in: Proceedings ICMS 2016 , 2016 , pp. 82 - 92 .

[9] D. Wilson , R. Bradford , J. Davenport , M. England , A “Piano Movers” Problem Reformulated, Technical Report CSBU-2013-03 Department of Computer Science University of Bath, 2013 .

[10] Z. Tonks , Poly-algorithmic Techniques in Real Quantifier Elimination , Ph.D. thesis , University of Bath, 2021 . URL: https://researchportal.bath.ac.uk/en/studentTheses/ poly -algorithmic-techniques-in-real-quantifier-elimination.

[11] Z. Tonks , A Poly-algorithmic Quantifier Elimination Package in Maple , in: J. Gerhard , I. Kotsireas (Eds.), Maple in Mathematics Education and Research 2019 , volume 1125 of Communications in Computer and Information Science, 2020 , pp. 171 - 186 .

[12] G. Collins, Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition , in: Proceedings 2nd. GI Conference Automata Theory & Formal Languages , 1975 , pp. 134 - 183 .

[13] S. McCallum , An Improved Projection Operation for Cylindrical Algebraic Decomposition , Ph.D. thesis , University of Wisconsin-Madison Computer Science, 1984 .

[14] D. Lazard , An Improved Projection Operator for Cylindrical Algebraic Decomposition , in: