### Algorithms Used

Several different algorithms are used depending on the problem and the input system. Two system options allow us to select which algorithms are used. Please note that the system option names and method names are strings.

This gives the methods used (with the current setting of the option) to solve the decision problem.

These algorithms are used in `ExistsRealQ`, `ForAllRealQ`, `ImpliesRealQ`, `InequalityInstance`, and in `Resolve` for systems with no free variables. The problem each of these functions is solving reduces to the problem of finding a solution of a system of equations and inequalities, or proving that the system has no solutions. Moreover, if the system is a disjunction, we look for solutions of each term separately, so in the following description the input system is a conjunction of equations and inequalities.

Let us describe the available methods in the order they are applied (provided the method is currently on the `RealPolynomialDecisionMethods` list and it is applicable to the input system).

`Simplex`. Used for linear equations and inequalities with rational or inexact coefficients. It is based on a modification of the Simplex linear optimization algorithm.

`LinearQE`. Used for linear equations and inequalities with exact coefficients. It is based on the linear quantifier elimination algorithm described in [7].

`LinearEquations`. Used as a preprocessor to other methods when there is a variable which appears at most linearly with a constant coefficient in an equation. Eliminates the variable using the equation.

`Groebner`. Used when input equations form a zero-dimensional ideal or generate all polynomials. Uses Groebner bases to find a solution.

`LWCCPreprocessor`. Used as a preprocessor to other methods when there is a variable which appears at most linearly with a constant coefficient in all equations and inequalities. Uses the linear quantifier elimination algorithm described in [7] to eliminate the variable.

`LWPreprocessor`. Used as a preprocessor to other methods when there is a variable which appears at most linearly in all equations and inequalities. Uses the linear quantifier elimination algorithm described in [7] to eliminate the variable.

`GenericCAD`. Used for systems of strong polynomial inequalities. It is based on the CAD algorithm, but uses a simpler projection and only rational sample points, as described in [11] (see also [10]).

`CAD`. Used for polynomial equations and inequalities with rational number coefficients. It is based on the cylindrical algebraic decomposition algorithm (see [1]). When equational constraints are present, we use the projection operator described in [2]. For well-oriented systems we use the projection operator described in [10]. For the general case we use the CAD algorithm with improvements described in [9], [6], and [3].

For other cases we use the following algorithms, which are the only algorithms available for the corresponding cases, so there is no option for switching them off.

· For algebraic equations and inequalities we replace algebraic numbers and functions with new variables, add suitable equations for the new variables, and use the CAD method. In the sample point construction phase of the CAD algorithm, we use the information that the new variables replace particular roots of the added equations.
· For nonlinear univariate polynomial equations and inequalities with nonrational coefficients, we use an algorithm based on numeric computation of roots of the polynomials.
· For nonlinear polynomial equations and inequalities with inexact coefficients, we use an algorithm based on CAD, described in [12].
· For nonlinear polynomials with exact nonalgebraic coefficients, we numericize the coefficients and use the algorithm described in [12].

Here are the methods used for quantifier elimination. They are used by `Resolve` when the input contains free variables.

Let us describe the available methods in the order in which they are applied (provided the method is currently on the `QuantifierEliminationMethods` list and it is applicable to the input system). The input system is written in the disjunctive normal form, i.e., a disjunction of conjunctions of equations and inequalities.

`LinearEquations`. Used whenever one of the variables of the innermost quantifier appears linearly with a constant coefficient in an equation which is present in all terms of the disjunction. Eliminates the variable by using the equation.

`LinearQE`. Used whenever one of the variables of the innermost quantifier appears at most linearly in all equations and inequalities. Eliminates the variable using the linear quantifier elimination algorithm described in [7].

`Groebner`. Used when equations common to all terms of the disjunctive form a zero-dimensional ideal or generate all polynomials. Computes a degrevlex Groebner basis and, using an algorithm based on [5], attempts to find equations in the ideal which are linear with a constant coefficient in one of the variables of the innermost quantifier. If successful, it eliminates the variable.

`CAD`. Used for polynomial equations and inequalities with rational coefficients. It is based on the CAD algorithm with the improvements described previously.

For algebraic equations and inequalities we replace algebraic numbers and functions with new variables, add suitable equations for the new variables, and use the CAD method with the new variables being the first ones to be projected out. In the sample point construction phase of the CAD algorithm, we use the information that the new variables replace particular roots of the added equations.

When variables are specified in `Resolve`, it will use the CAD method at the end to put the solution in the cylindrical solution form.

`InequalitySolve` (for multivariate algebraic equations and inequalities) and `CylindricalAlgebraicDecomposition` are using an algorithm based on CAD with the improvements described previously. In the univariate case `InequalitySolve` uses `Solve` to find all real zeros of the functions involved, and it determines the solution intervals by testing the inequalities at one point of each interval determined by the zeros.

`GenericCylindricalAlgebraicDecomposition` uses the projection described in [11] and constructs only rational sample points in full-dimensional cells. The hypersurface returned as the second element of the answer is constructed using the projection polynomials whose zeros are boundaries of the full-dimensional cells on which the input inequalities are satisfied.

`Minimize[`f`, `constr`, `vars`]` introduces an additional variable t, and it uses the CAD algorithm to find the smallest value of t for which the system of equations and inequalities has solutions. It selects the order of projections so that t is the last variable left. It takes roots of the polynomials in t and a rational point in each of the intervals determined by the roots and attempts to construct a sample point in the set of solutions of over the subsequent points, ordered by their values. If the first sample point constructed extends a root of one of the polynomials in t, then its t coordinate gives the minimum of f, and the remaining coordinates give a point satisfying the constraints at which the minimum is attained. Otherwise the infimum of f on the set of points satisfying the constraints is given by the largest root smaller than the t coordinate of the sample point, and the infimum is not attained.

`Infimum[`f`, `constr`, `vars`]` uses the same algorithm as `Minimize`, except that when constr contains only strong rational function inequalities, it uses the projection described in [11] and constructs only rational sample points in full-dimensional cells.

`Minimize` accepts an option `Experimental`WeakSolutions`. If this option is set to `True`, it uses the algorithm used by `Infimum` to find the infimum of values of f on the set of points satisfying the constraints, and then it attempts to find a point satisfying the weak versions of the constraint inequalities at which the infimum is attained. Note that such a point may not exist, or it may not belong to the closure of the set of points satisfying the constraints.

Converted by Mathematica      April 24, 2000

[Article Index] [Prev Page][Next Page]