This help page describes common keyword options relevant to routines provided in the QuantifierElimination package.

Routines within QuantifierElimination typically make use of the poly-algorithm implemented for quantifier elimination (QE), for which all options described below are relevant. In other words, options relevant to both virtual term substitution (VTS) and cylindrical algebraic decomposition (CAD) are relevant in the context of QE.

PartialCylindricalAlgebraicDecompose is an implementation of QE only using partial CAD, and hence only options for CAD are of relevance, including those for QE by CAD.

CylindricalAlgebraicDecompose is an implementation of "pure" CAD outside of the context of QE, and hence only those options from the section CAD below are relevant.

The poly-algorithmic routines (QuantifierEliminate, InsertFormula and DeleteFormula) will in practice only use CAD for QE when maxvsdegree = 0. Hence in this situation only the CAD-specific keyword options would be of relevance.

mode = identical( 'depth', 'breadth' )

determines how VTS selects subsequent operands for virtual substitution from the tree, or in other words how it traverses the VTS tree (default depth).

bounds = nonemptyset( identical( 'lower', 'upper' ) ) determines the bounds that VTS uses in test point generation (default { `lower` }).

hybridmode = identical( 'depth', 'breadth', 'whole' )

determines how QE uses CAD from VTS results when VTS can no longer be used for elimination due to excessive degree. depth or breadth means the poly-algorithm is used on the VTS tree depth or breadthwise, else the entire VTS tree is collapsed to one problem for CAD (default depth).

maxvsdegree = integer[ 0 .. 2 ]

determines the maximum degree of any polynomial factor VTS will consider using for quantifier elimination (default $2$).

processwitnesses = truefalse

flag that determines whether to process VTS prewitnesses into equations featuring real numbers in VTS (default true).

opencad = truefalse

flag determining whether it is permissible to construct an "open CAD". An open CAD is a CAD only constructing sectors over any cell, or in other words a CAD only featuring cells of full dimension (default false).

liftingconstraints = Or( set, identical( 'positive' ) )

a set of lifting constraints - inequalities on real linear polynomials in one variable each that describe maximal bound(s) to build CAD geometry in, or the symbol positive, requesting CAD to only construct geometry in positive real space (default $\varnothing$).

propagateecs = truefalse

flag determining whether equational constraints are propagated through projection, which leads to greater efficiency in the projection process (default true).

variablestrategy = Or( nonemptylist( name), identical( 'brown', 'tonks', 'ndrr', 'sotd', 'greedy' ) )

determines the name of the variable strategy to use within CAD, and hence how variables are sorted before (or during) projection, OR a list of variables to completely override the variable ordering, which must be a viable variable ordering for the formula/polynomials passed in terms of which variables are present, and the quantification of a formula if applicable (default tonks). Very brief descriptions of the strategies follow, while more in-depth descriptions of each of the strategies together with their origin can be found in [Ton21]. Note that while the last three strategies discussed below may require a significant time investment to decide a variable strategy, they can result in very competitive variable orderings for the purposes of cost of lifting. Hence they may overall result in a performance benefit ($n$ = number of variables).

brown: The "Brown heuristic" for variable ordering in CAD - prioritizes variables appearing at a lower degree in the input formula to be eliminated first in projection.

tonks: Like brown, but applied to equational constraints as a priority before applying to polynomials appearing from other contexts.

ndrr: Prioritizes the variable ordering leading to a projection set where the number of distinct real roots of the univariate projection basis is minimized. Note that this requires generation of $\mathrm{O}\left(n!\right)$ full projection sets.

sotd: Prioritizes the variable ordering leading to a projection set where the sum of the total degrees of polynomials across the projection bases is minimized. Note that this requires generation of $\mathrm{O}\left(n!\right)$ full projection sets.

greedy: Similar to sotd, but done variable by variable such that variables become successively fixed in the ordering when exploring all further possible projection bases. Similarly requires generation of $\mathrm{O}\left(n!\right)$ full projection sets, albeit fewer than for ndrr or sotd.

useequations = identical( 'none', 'single', 'multiple' )

determines how equational constraints should be used in restricted projection operations in projection. Usage of multiple equational constraints may result in mathematical exceptions ("curtains"), but usage of more equational constraints can increase performance considerably (default multiple). For more about this option, see the Equational Constraints with the Lazard Projection in CAD section of the QuantifierElimination example worksheet.

usegroebner = truefalse

flag determining whether equational constraints are preprocessed with Gröbner bases, which incurs some initial overhead, but may lead to greater efficiency later in projection (default true).

cellselectionstrategy = identical( 'HL_LI', 'TC_LD_HL_LI', 'TC_LD_HL_GI, 'SR_HL_LI' )

determines the cell selection strategy used in CAD for stack construction on cells (default HL_LI). This option is only relevant when using CAD in the context of quantifier elimination, where early termination criteria apply. The value passed defines a cell selection strategy in terms of tiebreakers between metrics on cells. The segments of the symbol delimited by underscores (_) represent metrics to use as part of the strategy. The following determines what the segments mean as part of these symbols in terms of a corresponding metric:

HL: "higher level",

LI: "least index",

LD: "least degree" (of the minimal polynomial defining the cell),

GI: "greatest index",

TC: "trivial conversion" (see [CH91]),

SR: "sectors first".

output = nonemptylist( identical( 'qf', 'witnesses', 'data' ) )

a list which defines which outputs will be provided and their sequential ordering. Each distinct symbol must appear at most once. These symbols correspond to:

qf: quantifier-free equivalent for QE.

witnesses: list of witnesses that prove equivalence of the quantified formula to its quantifier-free equivalent. Only applicable when the passed formula is fully quantified with only one quantifier symbol.

data: a QEData object when a poly-algorithmic method was used for elimination, else a CADData object. This object can be inspected via various object methods, or passed to routines such as InsertFormula or DeleteFormula for evolutionary QE.

The default value is always $\left[\mathrm{qf}\right]$.

eagerness = integer[1..3]

determines how eager QE should be to terminate once a sufficient quantifier-free equivalent for QE has been deduced (default 3). A lower value of eagerness may result in production of more witnesses when witnesses are requested via the keyword option output.

[CH91] Hong, H. and Collins, G.E. Partial Cylindrical Algebraic Decomposition for Quantifier Elimination. Journal of Symbolic Computation, pages 299–328, 1991.

[Ton21] Tonks, Z. Poly-algorithmic Techniques in Real Quantifier Elimination. PhD Thesis, University of Bath, UK, 2021.