Doctoral Thesis

SOLUTION FORMULA CONSTRUCTION FOR TRUTH-INVARIANT CADs

ABSTRACT

The CAD-based quantifier elimination algorithm takes a formula from the elementary theory of real closed fields as input, and constructs a CAD of the space of the formula's unquantified variables. This decomposition is truth invariant with respect to the input formula, meaning that the formula is either identically true or identically false in each cell of the decomposition. The method determines the truth of the input formula for each cell of the CAD, and then uses the CAD to construct a solution formula --- a quantifier free formula that is equivalent to the input formula. This final phase of the algorithm, the solution formula construction phase, is the focus of this thesis.

An optimal solution formula construction algorithm would be complete --- i.e. applicable to any truth-invariant CAD, would be efficient, and would produce simple solution formulas. Prior to this thesis, no method was available with even two of these three properties. Several algorithms are presented , all addressing problems related to solution formula construction. In combination, these provide an efficient and complete method for constructing solution formulas that are simple in a variety of ways.

Algorithms presented in this thesis have been implemented using the SACLIB library, and integrated into QEPCAD, a SACLIB-based implementation of quantifier elimination by CAD. Example computations based on these implementations are discussed.