Return to numtr.tex CVS log

Up to [local] / OpenXM / src / asir-doc / papers

Annotation of OpenXM/src/asir-doc/papers/numtr.tex, Revision 1.1

1.1     ! noro        1: \documentstyle[12pt,psfig,amssymb,isisrr]{article}
        !             2: \newcommand{\msub}{/\kern-3pt/}
        !             3: \rrno{5E}
        !             4: \isismemo
        !             5: \Email{sturm}
        !             6: \abstract{Weispfenning has shown how to use test term methods for quantifier
        !             7: elimination in linear and quadratic first-order formulas over real
        !             8: closed fields. This paper describes the state of the implementation of
        !             9: such methods in the computer algebra system Risa/Asir. The package
        !            10: described here is entirely written in the C programming language. We
        !            11: point on possible extensions of the package and give examples for
        !            12: automatic quantifier eliminations performed by Risa/Asir.}
        !            13: \keywords{real quantifier elimination, parametric constraint solving,
        !            14: implementation, Asir package}
        !            15: \begin{document}
        !            16: \title{Real Quadratic Quantifier Elimination\\ in Risa/Asir}
        !            17: \author{Thomas Sturm\thanks{Visiting researcher. Original affiliation:
        !            18: Fakult\"at f\"ur Mathematik und Informatik, Universit\"at Passau,
        !            19: D-94030 Passau, Germany. Email: sturm@fmi.uni-passau.de.}}
        !            20: \maketitle
        !            21: %
        !            22: \section{Introduction}
        !            23: A {\em quantifier elimination procedure} is an algorithm that, given a
        !            24: first order formula, computes an equivalent quantifier-free formula. A
        !            25: quantifier elimination procedure for the reals has been given already
        !            26: by Tarski~\cite{Tarski:48}. Due to the enormous power of such
        !            27: algorithms efforts to implement them have been made from the very
        !            28: beginning on. In fact the US RAND Corporation had soon tried to
        !            29: implement the original Tarski procedure, which certainly failed at
        !            30: those days.
        !            31:
        !            32: The first complete implementation by Arnon was finished in 1981
        !            33: \cite{Arnon:81}. It used the cylindrical algebraic decomposition
        !            34: method by Collins~\cite{Collins:75}. This implementation of quantifier
        !            35: elimination triggered the development of one of the first computer
        !            36: algebra systems: SAC, now SAC-II/ALDES. Important improvements of the
        !            37: CAD method have been made by Collins and Hong~\cite{CollinsHong:91}
        !            38: resulting in the {\em partial} CAD implemented in Hong's QEPCAD
        !            39: package~\cite{Hong:93}.
        !            40:
        !            41: Weispfenning introduced an alternative approach to quantifier
        !            42: elimination first for linear formulas \cite{Weispfenning:88}. This
        !            43: could be extended to arbitrary degrees
        !            44: \cite{LoosWeispfenning:93,Weispfenning:96,Weispfenning:94}. For
        !            45: degrees $1$ and $2$, the methods have been successfully implemented in
        !            46: the REDUCE package REDLOG written by the author and others
        !            47: \cite{DolzmannSturm:95a,DolzmannSturm:96}. Despite the bad theoretical
        !            48: complexity~\cite{Weispfenning:88,Davenport:88} and the degree
        !            49: restrictions REDLOG turned out suitable for solving a number of
        !            50: practical problems \cite{Weispfenning:95b,Weispfenning:96b}. Meanwhile
        !            51: it is used commercially as part of an error diagnosis system for
        !            52: physical networks.
        !            53:
        !            54: We have now started a second implementation of the test term method in
        !            55: the C language using the Risa/Asir computer algebra system
        !            56: \cite{NoroTakeshima:92}. The aim of this reimplementation is twofold.
        !            57: On one hand, we may expect to achieve a gain in efficiency due to both
        !            58: the C language and the efficient polynomial algorithms present in
        !            59: Risa. On the other hand we wish to make the methods available to
        !            60: interested parties in industry where C is still the most widespread
        !            61: programming language.
        !            62:
        !            63: The purpose of this report is to summarize the state of the
        !            64: reimplementation after an initial phase of eight weeks. We further
        !            65: point on features to be added. All these features are already part of
        !            66: the REDLOG package.
        !            67: %
        !            68: \section{Description of the implementation}
        !            69: In the sequel, we assume the reader to be familiar with the theory of
        !            70: quantifier elimination by test term methods as it has been described
        !            71: by Weispfenning \cite{LoosWeispfenning:93,Weispfenning:96}.
        !            72: Figure~\ref{modstruct} shows the module structure of the packege.
        !            73: \begin{figure}
        !            74: \centerline{\psfig{figure=qe2.eps,width=0.8\textwidth}}
        !            75: \caption{Visualisation of the module interaction\label{modstruct}}
        !            76: \end{figure}
        !            77: \subsection{Functionality}
        !            78: The current implementation can eliminate existential and universal
        !            79: quantifiers from prenex first-order formulas, subject to the
        !            80: restriction that with the elimination of each variable the latter
        !            81: occurs at most quadratically within the quantified {\em matrix}
        !            82: formula. This includes the technique described in
        !            83: \cite{Weispfenning:96} where in a situation as
        !            84: $$
        !            85: \exists x\bigl(a_2x^2+a_1x+a_0=0\land\varphi\bigr)
        !            86: $$
        !            87: at least one of $a_2$, $a_1$, $a_0$ is a non-zero number. The
        !            88: quantified variable $x$ may then occur with arbitrary degree in
        !            89: $\varphi$. We refer to this special case as {\em Gauss elimination}
        !            90: treated in Subsection~\ref{gaussnow}.
        !            91:
        !            92: Furthermore, there are some minor tool functions operating on formulas
        !            93: available. All functions are listed and described briefly in the
        !            94: Appendix~\ref{doku}.
        !            95:
        !            96: \subsection{Toplevel elimination}
        !            97: The quantifier elimination routine is called with a prenex first-order
        !            98: formula. This formula is simplified, and then turned into {\em
        !            99: negation normal form}, i.e., a prenex formula the matrix of which
        !           100: contains only $\land$ and $\lor$ as first-order operators. Next the
        !           101: formula is split into a list of quantifier block and its matrix.
        !           102:
        !           103: The elimination of universal quantifiers blocks is reduced to that of
        !           104: existential ones using the equivalence $\forall
        !           105: x\varphi\longleftrightarrow \lnot\exists x\lnot\varphi$. We shall
        !           106: restrict our attention to existential quantifiers from now on.
        !           107:
        !           108: For each block, beginning with the innermost, there is a routine
        !           109: called that is designed to eliminate one prenex existential quantifier
        !           110: block.
        !           111: %
        !           112: \subsection{Quantifier blocks}
        !           113: A block of quantifiers $\exists x_n\ldots\exists x_1$ is eliminated
        !           114: successesively beginning with the innermost quantifier. Let $E_1$ be
        !           115: an elimination set for the innermost quantifier $\exists x_1$ we
        !           116: obtain a formula
        !           117: $$
        !           118: \exists x_n\ldots\exists x_2\bigvee_{t\in E_1}\varphi[x\msub t].
        !           119: $$
        !           120: The remaining quantifiers can be moved inside the disjunction. The
        !           121: branches obtained are eliminated independently decreasing the overall
        !           122: complexity from doubly to singly exponential.
        !           123:
        !           124: This technique is implemented by processing a {\em queue} of {\em
        !           125: subproblems}. A subproblem is a pair $(V_{ij},\psi_{ij})$ consisting
        !           126: of an (existentially quantified) variable list $V_{ij}$ and a matrix
        !           127: formula $\psi_{ij}$. With the substitution of an elimination set for a
        !           128: certain variable we do not construct a disjuntion but instead add the
        !           129: results still containing quantified variables as new subproblems to a
        !           130: problem queue called {\em container}. The completely eliminated
        !           131: subproblems ($V_{nj}=\emptyset$) are, in contrast, added to a {\em
        !           132: result box}.
        !           133:
        !           134: The subproblems obtained this way form a tree by branching from each
        !           135: subproblem to its child problems until its leafs eventually enter the
        !           136: result box. The depth of this {\em elimination tree} is the number of
        !           137: variables in the initial $V_{11}$. Its width at each level is the sum
        !           138: of the sizes of the elimination sets obtained from the nodes of the
        !           139: parent level.
        !           140:
        !           141: Choosing a queue for storing subproblems amounts to computing the
        !           142: elimination tree in a {\em breadth first search} (BFS) manner. The
        !           143: advantage of BFS is that equal sibling nodes can be detected when
        !           144: adding to the container. This prevents the recomputation of identical
        !           145: subtrees.
        !           146:
        !           147: The procedure terminates when the container gets empty. This happens
        !           148: after finitely many steps according to K\"onig's Lemma. Finally a
        !           149: disjunction is constructed from the content of the result box.
        !           150:
        !           151: A subproblem $(V_{ij},\psi_{ij})$ is processed by first trying Gauss
        !           152: elimination for $V_{ij}$ and $\psi_{ij}$. If this succeeds, an
        !           153: elimination set is obtained from the Gauss elimination routine. Else a
        !           154: translation is computed for the first (innermost) variable of $V_{ij}$
        !           155: and the matrix $\psi_{ij}$. This translation is turned into an
        !           156: elimination set by yet another routine. Elimination sets are
        !           157: substituted elementwise. Each substitution result is simplified and
        !           158: becomes a new subproblem with one variable less.
        !           159:
        !           160: Notice that our container technique allows to eliminate the variables
        !           161: in a different order for each branch of the tree. The Gauss
        !           162: elimination already makes use of this feature.
        !           163: %
        !           164: \subsection{Gauss elimination}\label{gaussnow}
        !           165: The Gauss elimination routine first checks alle variables trying to
        !           166: find a possibility for a linear Gauss step, i.e. one in which the
        !           167: coefficient $a_2$ of $x_2$ is zero. Such an elimination does not
        !           168: increase the degree of the other variables. If this fails, it checks
        !           169: for a quadratic Gauss. If the Gauss routine detects a Gauss situation,
        !           170: it returns an elimination set to be substituted by the block
        !           171: elimination routine. Else it signals its failure.
        !           172: %
        !           173: \subsection{Translation stage}
        !           174: The test term technique ist based on testing endpoints of intervals
        !           175: including $\pm\infty$ and possibly adding or subtracting some
        !           176: infinitesimal $\epsilon$. In the translation phase all endpoint
        !           177: candidates are collected and classified wrt.~their {\em bounding type}
        !           178: and their {\em infinity type}.
        !           179:
        !           180: The bounding type encodes the relevant information on the constraint
        !           181: that has delivered the point. Table~\ref{bttab} collects the bounding
        !           182: types currently used.
        !           183: %
        !           184: \begin{table}[t]
        !           185: \begin{center}
        !           186: \begin{tabular}{ll}
        !           187: \hline
        !           188: BTEQUAL & Equation: $p$\\
        !           189: BTNEQ & Inequality: ${\Bbb R}\setminus\{p\}$\\
        !           190: BTLEQ & Weak upper bound: $]-\infty,p]$\\
        !           191: BTGEQ & Weak lower bound: $[p,\infty[$\\
        !           192: BTLESSP & Strict upper bound: $]-\infty,p[$\\
        !           193: BTGREATERP & Strict lower bound: $]p,\infty[$\\
        !           194: BTWO & Weak ordering: Weak lower or upper bound\\
        !           195: BTSO & Strict ordering: Strict lower or upper bound\\
        !           196: \hline
        !           197: \end{tabular}
        !           198: \end{center}
        !           199: \caption{Interpretation of an endpoint $p$ according to its bounding
        !           200: type.\label{bttab}}
        !           201: \end{table}
        !           202: %
        !           203: By the way of example, consider $4x-7\geq0$, which contributes $7/4$
        !           204: as a lower bound on $x$, i.e., BTGEQ. In contrast, $ax-7\geq0$ does
        !           205: not contribute a lower bound; for $a<0$ it is an upper bound. Thus the
        !           206: bounding type for $7/a$ in the latter example is BTWO.
        !           207:
        !           208: Table~\ref{ittab} collects the infinity types and their relation to
        !           209: the bounding types.
        !           210: %
        !           211: \begin{table}[t]
        !           212: \begin{center}
        !           213: \begin{tabular}{lll}
        !           214: \hline
        !           215: infinity type & occurs with & interpretation\\
        !           216: \hline
        !           217: STD & BTEQUAL & $p$\\
        !           218: EPS & BTSO, BTNEQ & $p$ plus {\em or} minus $\epsilon$\\
        !           219: MEPS & BTLESSP & $p-\epsilon$\\
        !           220: PEPS & BTGREATERP & $p+\epsilon$\\
        !           221: PINF & --- & $\infty$\\
        !           222: MINF & --- & $-\infty$\\
        !           223: \hline
        !           224: \end{tabular}
        !           225: \end{center}
        !           226: \caption{Interpretation of an endpoint $p$ according to its infinity
        !           227: type. Infinity types are related to bounding types.\label{ittab}}
        !           228: \end{table}
        !           229: %
        !           230: Points of infinity type $\epsilon$ are {\em unspecified}, all others
        !           231: are {\em specified}. The types PINF and MINF are not used at the
        !           232: translation stage.
        !           233:
        !           234: Taking a point labeled with its infinity type and adding conditions
        !           235: for its existence and its relevance yields a {\em guarded point}.
        !           236: Solutions $-c/b$ of linear contraints are guarded by $b\neq 0$.
        !           237: Solutions $(-b\pm\sqrt{b^2-4ac})/2a$ of quadratic contraints are
        !           238: guarded by $a\neq0\land b^2-4ac\geq0$.
        !           239:
        !           240: Finally, for a fixed variable a {\em translation} is an array, indexed
        !           241: by bounding types, of sets of guarded points obtained from the
        !           242: constraints in the matrix formula.
        !           243:
        !           244: Actually, the endpoints are not stored as explicit terms but in the
        !           245: form of minimal polynomials. Consequently, one point can stand for
        !           246: several roots in case of quadratic constraint. Notice that all the
        !           247: roots are assigned both the same infinity type and bounding type.
        !           248:
        !           249: On the other hand, one constraint can in fact produce several guarded
        !           250: points. For instance, consider the contraint $ax^2+5x+c\geq0$. This
        !           251: yields a two-root guarded point
        !           252: $$
        !           253: \bigl(a\neq0\land 25-4ac\geq0,(ax^2+5x+c,\mbox{STD})\bigr)
        !           254: $$
        !           255: of bounding type BTWO. On the other hand, for $a=0$ it is a hidden
        !           256: linear constraint. Hence we additionally obatin
        !           257: $(5\neq0,(5x+c,\mbox{STD}))$ of bounding type BTGEQ.
        !           258:
        !           259: The translation array is the input to the elimination set computation
        !           260: routine.
        !           261: %
        !           262: \subsection{Elimination set computation}
        !           263: An elimination set is a single set of guarded points non of which is
        !           264: unspecified wrt.~its infinity type. Given a translation there are thus
        !           265: three tasks to be performed.
        !           266: \begin{enumerate}
        !           267: \item Choose a small selection of guarded points for obtaining an
        !           268: elimination set.
        !           269: \item Specify each unspecified guarded point (of infinity type EPS) in
        !           270: this selection to either PEPS or MEPS.
        !           271: \item Add elements that are not induced by isolated contraints to the
        !           272: elimination set.
        !           273: \end{enumerate}
        !           274: %
        !           275: The current implementation decides between either taking all upper
        !           276: bounds or all lower bounds depending on the number of such bounds
        !           277: present. Accordingly, EPS is sepcified to either MEPS or PEPS, and
        !           278: either $(0=0,(0,\mbox{PINF}))$ or $(0=0,(0,\mbox{MINF}))$ is added. If
        !           279: there are no orderings at all, $(0=0,(x,\mbox{STD}))$, i.e., ``$0$''
        !           280: is added instead of an infinite value. Mind that at least one point
        !           281: has to be substituted for the case that none of the guards holds.
        !           282:
        !           283: Summarizing, the bounding type provides information concerning the
        !           284: selection of a proper subset of the translation. The infinity type
        !           285: provides information concerning the substitution. The infinity type
        !           286: cannot always be completely determined at the translation stage.
        !           287: %
        !           288: \subsection{Substitution}
        !           289: In an object oriented style, there is one procedure that can
        !           290: substitute a guarded point into a formula. The sustitution module
        !           291: includes substitution of infinite and infinitesimal symbols and
        !           292: substitution of root expressions within the language of ordered rings.
        !           293: The methods used are that described in \cite{Weispfenning:96}. We make
        !           294: use of our minimal polynomial representation for the roots by
        !           295: performing pseudo divison before symbolically substituting.
        !           296: %
        !           297: \subsection{Simplification}\label{currentsimpl}
        !           298: Currently, the following simplification strategies are applied:
        !           299: \begin{itemize}
        !           300: \item
        !           301: Evaluation of variable-free atomic formulas.
        !           302: \item
        !           303: Replacing equation and inequality right hand sides by their squarefree
        !           304: part. Corresponding treatment of ordering atomic formulas: Here
        !           305: factors of even multiplicity have to enter squared.
        !           306: \item
        !           307: Removing \verb!true! from conjunctions, \verb!false! from
        !           308: disjunctions. Conjunctions containing \verb!false! and disjunctions
        !           309: containing \verb!true! are replaced by the respective truth value.
        !           310: Truth values are treated appropriately also with all other first-order
        !           311: operators.
        !           312: \item
        !           313: Removing equal subformulas from conjunctions and disjunctions. Atomic
        !           314: subformulas are ordered canonically and placed before their complex
        !           315: siblings. The order of atomic formulas is first wrt.~their left hand
        !           316: side polynomial, and then wrt.~the order of relations as in
        !           317: Table~\ref{atoptab}.
        !           318: \end{itemize}
        !           319: %
        !           320: \section{Possible Extensions}\label{genopt}
        !           321: We point on possible extension of the Asir quantifier elimination
        !           322: code. All options mentioned here are already part of the REDLOG
        !           323: package~\cite{DolzmannSturm:95a,DolzmannSturm:96}. They have been
        !           324: extensively tested for their relevance.
        !           325: \subsection{Functionality}
        !           326: For many practical applications, it is necessary to add an option for
        !           327: {\em extended quantifier elimination:} This variant keeps track of the
        !           328: test points substituted. With the elimination of an existential
        !           329: quantifier block, it provides instead of a disjunction
        !           330: $\bigvee_{i=1}^n \psi_i$ a set of {\em guarded points}
        !           331: $$
        !           332: \bigl\{(\psi_1,S_1),\dots,(\psi_n,S_n)\bigr\}
        !           333: $$
        !           334: such that whenever an interpretation of the parameters satisfies some
        !           335: $\psi_i$, the original $\exists$-quantified formula holds for this
        !           336: interpretation, and $S_i$ provides some sample values for the
        !           337: quantified variables possibly containing $\pm\epsilon$ or $\pm\infty$.
        !           338:
        !           339: The extension of the package to {\em generic quantifier
        !           340: elimination}~\cite{DSW:96} is of the same importance. There, the
        !           341: quantifier elimination procedure is allowed to make certain assumption
        !           342: of the form $t\neq0$ for parameter term $t$. These assumptions support
        !           343: the elimination process leading to a much smaller result, which is
        !           344: correct under~the assumptions. Of course, the list of assumptions made
        !           345: is also returned to the caller. It has turned out that for the
        !           346: majority of practical applications, the assumptions made are
        !           347: ``harmless''. They describe some degenerate cases, which are actually
        !           348: not relevant.
        !           349:
        !           350: Finally, the package should not be restricted to quantifier
        !           351: elimination itself but also include other useful algorithms on
        !           352: formulas such as CNF/DNF computation or advanced simplifiers for final
        !           353: results.
        !           354: %
        !           355: \subsection{Toplevel elimination}
        !           356: There should be code added for making formulas prenex such that the
        !           357: quantifier elimination can be called with arbitrary formulas.
        !           358: %
        !           359: \subsection{Quantifier blocks}\label{blockopt}
        !           360: There should be an option added to use a stack instead of a queue as
        !           361: container. This amounts to a DFS computation of the elimination tree.
        !           362: The advantage is that with (wlog.~existential) decision problems, one
        !           363: has a good chance to detect a ``true'' leaf early. Computation can be
        !           364: aborted then. For the elimination of several blocks in a decision
        !           365: problem it is useful to switch dynamically from BFS to DFS.
        !           366:
        !           367: A variable selection strategy has to be added. For instance, linear
        !           368: variables have to be preferred because their elimination does not
        !           369: increase the degree of the other variables.
        !           370:
        !           371: Some techniques for reducing the degree of the quantified variables
        !           372: take into account the whole formula \cite{DSW:96}. They should be
        !           373: applied at this stage.
        !           374: %
        !           375: \subsection{Gauss elimination}
        !           376: The Gauss elimination code already prefers linear variables. It should
        !           377: check all possibilities yet more closely: among linear equations,
        !           378: e.g., $x=0$ should be preferred to $ax+1=0$ since the former does not
        !           379: introduce a guarding condition.
        !           380:
        !           381: One should try to factorize polynomials of a degree greater than $2$.
        !           382: %
        !           383: \subsection{Translation stage}
        !           384: At the translation stage, one also should try to factorize polynomials
        !           385: of a degree greater than $2$. The current implementation aborts with
        !           386: an error in such a case. Even if factorization fails, the computation
        !           387: should be continued. The result can be requantified, and with an
        !           388: (wlog.~existential) decision problem, one still has the chance to find
        !           389: ``true''.
        !           390: %
        !           391: \subsection{Elimination set computation}
        !           392: There are numerous sophisticated techniques for constructing small
        !           393: elimination sets from a translation.
        !           394: %
        !           395: \subsection{Simplification}
        !           396: Due to the doubly exponential explosion in the number of atomic
        !           397: fomulas, simplification plays an extremely important role with this
        !           398: method. Appropriate simplifications are described in detail in
        !           399: \cite{DolzmannSturm:95}.
        !           400: %
        !           401: \section{Computation examples}
        !           402: All the following examples have been computed on a SUN Sparc-20.
        !           403: \subsection{The Davenport--Heintz Example}
        !           404: This example is taken from \cite{CollinsHong:91}, p.\,325. The formula
        !           405: $$
        !           406: \exists c \forall a \forall b(a=d \land b=c) \lor (a=c \land b=1)
        !           407: \longrightarrow a^2=b))
        !           408: $$
        !           409: is a special case of more general formula used by Davenport and Heintz
        !           410: \cite{Davenport:88} in order to show the time complexity of real
        !           411: quantifier elimination. It is equivalent to $d=1\lor d=-1$. Asir
        !           412: yields after $0.03$\,s the equivalent result
        !           413: $$
        !           414: \vbox{\hsize=0.9\textwidth\noindent$d^{4} - 1 = 0 \land d \neq 0 \land
        !           415: (d = 0 \lor d \neq 0) \land (d= 0 \lor d \neq 0 \land (d^{2} - 1 \neq
        !           416: 0 \lor d \neq 0)) \land (d^{3} - d = 0 \lor d^{2}- d \neq 0 \land
        !           417: d^{2} - 1 \neq 0) \land (d^{2} - 1 \neq 0 \lor d \neq 0) \land (d^{2} -
        !           418: 1 = 0 \lor d^{2} - d \neq 0 \land d^{2} - 1 \neq 0)$}
        !           419: $$
        !           420: The REDLOG standard simplifier can simplify this to $d \neq 0 \land (d
        !           421: + 1= 0 \lor d - 1 = 0)$. This points on the necessity of more
        !           422: sophisticated simplification strategies.
        !           423: %
        !           424: \subsection{Transportation problem}
        !           425: An example which should not suffer from missing simplification is the
        !           426: 2-dimensional planar $3\times 3$ transportation problem taken from
        !           427: \cite{LoosWeispfenning:93}, pp.\,459/460. The input formula
        !           428: $$
        !           429: \exists x_{11}\exists x_{12}\exists x_{13}\exists x_{21}\exists
        !           430: x_{22}\exists x_{23}\exists x_{31}\exists x_{32}\exists x_{33}\biggl(
        !           431: \bigwedge_{i=1}^3\bigwedge_{j=1}^3 x_{ij}\geq0\land
        !           432: \bigwedge_{k=1}^3\Bigl(\sum_{j=1}^3 x_{kj}=a_k\land \sum_{i=1}^3
        !           433: x_{ik}=b_k\Bigr) \biggr)
        !           434: $$
        !           435: is known to be equivalent to $\sigma\equiv\bigwedge_i (a_i\geq0) \land
        !           436: \bigwedge_j (b_j\geq0) \land \sum_i a_i=\sum_j b_j$. After $0.31$\,s
        !           437: Asir yields a quantifier-free equivalent $\rho$ containing $84$ atomic
        !           438: formulas. So does REDLOG. We automatically check $\forall a_1\forall
        !           439: a_2\forall a_3\forall b_1\forall b_2 \forall
        !           440: b_3(\rho\longleftrightarrow\sigma)$ obtaining ``true'' after
        !           441: $47.83$\,s plus $36.04$\,s GC time.
        !           442: %
        !           443: \subsection{Kahan's Problem}
        !           444: Write down conditions such that the ellipse $E(x,y)=0$ with
        !           445: $$
        !           446: E(x,y)=(x-c)^2/a^2+(y-d)^2/b^2-1
        !           447: $$
        !           448: is inside the circle $C(x,y)=0$ with $C(x,y)=x^2+y^2-1$
        !           449: \cite{Lazard:88}. We treat the special case $d=0$. Eliminating
        !           450: $$
        !           451: \forall a\forall b\bigl(b^2 (x-c)^2+a^2 y^2-a^2 b^2 \neq 0 \lor
        !           452: x^2+y^2-1 \leq 0\bigr)
        !           453: $$
        !           454: we obtain after $1.21$\,s plus $0.14$\,s GC time a quantifier-free formula
        !           455: containing $136$ atomic formulas. REDLOG obtains only $59$ atomic
        !           456: formulas due degree decreasing techniques, better simplification, and
        !           457: more sophisticated elimination set computation ($2.9$\,s).
        !           458: %
        !           459: \subsection{Operation amplifier}
        !           460: This is a problem very close to practice taken from \cite{Henning:91}.
        !           461: \begin{figure}
        !           462: \centerline{\psfig{figure=db15.ps}}
        !           463: \caption{An inverting operation amplifier circuit\label{opampfig}}
        !           464: \end{figure}
        !           465: For the operation amplifier circuit shown in Figure~\ref{opampfig}, we
        !           466: want to determine the output voltage $\rm V_{OUT}=v1$ as a function of
        !           467: the input voltage $\rm V_{IN}=v\_3$. We obtain the following algebraic
        !           468: formulation $\omega$ of the circuit:
        !           469: $$\vbox{\hsize=0.9\textwidth\noindent$\rm -v\_2+v\_1+i\_v0\cdot r1=0
        !           470: \land -v\_3\cdot r1+v\_2\cdot r1+v\_2\cdot r2-v\_1\cdot
        !           471: r2-i\_pm\_op1\cdot r1\cdot r2=0 \land v\_3-v\_2+i\_og\_op1\cdot r2=0
        !           472: \land v\_1=v1 \land v\_3-v\_og\_op1=0 \land - v\_pm\_op1-v\_2=0 \land
        !           473: vs^2\cdot x\_op1^2+a\cdot v\_og\_op1^2=a\cdot vs^2 \land
        !           474: v\_og\_op1=v\_pm\_op1\cdot x\_op1^2 \land i\_pm\_op1=0$}
        !           475: $$
        !           476: The variables to be (existentially) eliminated are
        !           477: $$\rm
        !           478: V:=\{i\_og\_op1, v\_2, i\_pm\_op1, v\_1, i\_v0, v\_pm\_op1, v\_og\_op1 ,
        !           479: x\_op1\}
        !           480: $$
        !           481: For the values $\rm a=1000$, $\rm vs=10$, $\rm r1=1000$, and $\rm
        !           482: r2=10000$ the translation $\omega$ specializes to the following
        !           483: $\omega'$:
        !           484: $$\vbox{\hsize=0.9\textwidth\noindent$\rm
        !           485: 10000\cdot i\_og\_op1 - v\_2 + v\_3 = 0 \land 10000\cdot i\_pm\_op1 +
        !           486: 10\cdot v\_1 - 11\cdot v\_2 + v\_3 = 0 \land i\_pm\_op1 = 0 \land
        !           487: 1000\cdot i\_v0 + v\_1 - v\_2 = 0 \land v1 - v\_1 = 0 \land v\_2 +
        !           488: v\_pm\_op1 = 0 \land v\_3 - v\_og\_op1 = 0 \land 10\cdot v\_og\_op1^2
        !           489: + x\_op1^2 - 1000 = 0 \land v\_og\_op1 - v\_pm\_op1\cdot x\_op1^2 =
        !           490: 0$}
        !           491: $$
        !           492: A symbolic method usually used for eliminating the variables is the
        !           493: computation of an {\em elimination ideal basis} wrt.~the variables.
        !           494: Using this method, we obtain by using Asir
        !           495: $$\rm
        !           496: f:=10\cdot v\_3^3+100\cdot v1\cdot v\_3^2-1011\cdot v\_3-10000\cdot v1
        !           497: $$
        !           498: as implicit description of our function.
        !           499: \begin{figure}
        !           500: \centerline{\psfig{figure=parsol.ps,width=0.8\textwidth}}
        !           501: \caption{The operation amplifier's behaviour including parasitic
        !           502: solutions for $\rm |v\_3|>10$.\label{solfig}}
        !           503: \end{figure}
        !           504: Figure~\ref{solfig} displays the set of {\em real} zeroes of $f$.
        !           505: However, only the part of the curve for $\rm -10\leq v\_3\leq10$ is
        !           506: the correct solution. The other parts are {\em parasitic solutions}
        !           507: caused by the fact that the elimination ideal is computed over an
        !           508: algebraically closed field, such as $\Bbb C$ for our case. In general,
        !           509: it is a problem to distinguish between proper and parasitic solutions.
        !           510:
        !           511: Since our quantifier elimination is a {\em real} method, we may expect
        !           512: to get the correct result. The current Asir version is not able to
        !           513: eliminate $\exists V(\omega')$. It would obtain a degree violation
        !           514: when eliminating $\rm x\_op1$ as the final variable. Its degree will
        !           515: be greater than $2$ then. We can, however, apply a special case of the
        !           516: degree decreasing methods mentioned in Subsection~\ref{blockopt} by
        !           517: hand: $\rm x\_op1$ occurs only quadratically. We replace $\rm
        !           518: x\_op1^2$ by a new variable $z$ in $\omega'$ obtaining $\omega_z'$.
        !           519: Similarly we replace $\rm x\_op1$ by $z$ in $V$ yielding $V_z$. Then
        !           520: we have the equivalence
        !           521: $$
        !           522: \exists V(\omega')\longleftrightarrow\exists V_z(\omega_z'\land
        !           523: z\geq0),
        !           524: $$
        !           525: the right hand side of which can be eliminated. The result obtained
        !           526: after $0.03$\,s contains the correct contraint on the range of $\rm
        !           527: v\_3$ to exclude the parasitic solutions:
        !           528: $$\rm \underbrace{10\cdot v\_3^3+100\cdot v1\cdot v\_3^2-1011\cdot
        !           529: v\_3-10000\cdot v1}_{\mathit f}=0 \land v\_3^2-100 \leq 0.
        !           530: $$
        !           531:
        !           532: Inspection of this example shows that there is actually only Gauss
        !           533: elimination performed, which is a little disappointing. For
        !           534: demonstrating the power of the method, we show how to solve the
        !           535: original parametric problem with REDLOG: For $\exists V(\omega)$, we
        !           536: obtain $604$ atomic formulas after $2.69$\,s. A result of this size
        !           537: might be useful for further automatic processing but it does not
        !           538: immediately contribute to understanding the network.
        !           539:
        !           540: We thus apply {\em generic quantifier elimination} as proposed in
        !           541: Subsection~\ref{genopt}. The result obtained for $\exists V(\omega)$
        !           542: after $0.27$\,s is:
        !           543: $$\vbox{\hsize=0.9\textwidth\noindent$\rm
        !           544: a\cdot r1\cdot v\_3^3 - a\cdot r1\cdot v\_3\cdot vs^2 + a\cdot r2\cdot
        !           545: v1\cdot v\_3^2 - a\cdot r2\cdot v1\cdot vs^2 - r1\cdot v\_3\cdot vs^2 -
        !           546: r2\cdot v\_3\cdot vs^2 = 0 \land a\cdot v\_3^2 - a\cdot vs^2 \leq 0 \land
        !           547: vs \neq 0$},
        !           548: $$
        !           549: valid under the following conditions:
        !           550: $$\rm
        !           551: a \neq 0,\quad r1 \neq 0,\quad r2 \neq 0,\quad v_3 + vs \neq 0,\quad
        !           552: v_3 - vs \neq 0,\quad v_3 \neq 0.
        !           553: $$
        !           554: None of the conditions is a problem: $\rm a$ is the amplification
        !           555: factor, $\rm r1$ and $\rm r2$ are resistors, the absolute value of the
        !           556: output voltage $\rm v\_3$ can certainly never get equal to the supply
        !           557: power $\rm vs$.
        !           558: %
        !           559: \begin{appendix}
        !           560: \section{The Asir user interface}\label{doku}
        !           561: \subsection{The formula data type}
        !           562: For the purpose of quantifier-elimination formulas have been
        !           563: introduced to Asir as a new data type. The numerical value
        !           564: corresponding to formulas is $10$. Atomic formula operators are
        !           565: collected in Table~\ref{atoptab}.
        !           566: \begin{table}
        !           567: \begin{center}
        !           568: \begin{tabular}{c|c|c|c|c|c}
        !           569: $=$ & $\neq$ & $\leq$ & $<$ & $\geq$ & $>$\\
        !           570: \hline
        !           571: \verb"@==" (\verb"@=") & \verb"@!=" & \verb"@<=" & \verb"@<" &
        !           572: \verb"@>=" & \verb"@>"\\
        !           573: \end{tabular}
        !           574: \caption{Infix operators for the input of atomic formulas
        !           575: (abbreviations for input).\label{atoptab}}
        !           576: \end{center}
        !           577: \end{table}
        !           578: The First-order operators are displayed in Table~\ref{coptab}.
        !           579: \begin{table}
        !           580: \begin{center}
        !           581: \begin{tabular}{c|c|c|c|c|c|c|c}
        !           582: $\land$ & $\lor$ & $\lnot$ & $\longrightarrow$ & $\longleftarrow$ &
        !           583: $\longleftrightarrow$ & $\exists x\ldots$ & $\forall x\ldots$\\
        !           584: \hline
        !           585: \verb"@&&" & \verb"@||" & \verb"@!" & \verb"@impl" & \verb"@repl" &
        !           586: \verb"@equiv" & \verb"ex(x,...)" & \verb"all(x,...)" \\
        !           587: (\verb"@&") & (\verb"@|") & & & & & &\\
        !           588: \end{tabular}
        !           589: \caption{Binary and infix operators for the input of first-order
        !           590: formulas (abbreviations for input).\label{coptab}}
        !           591: \end{center}
        !           592: \end{table}
        !           593:
        !           594: We illustrate by example the input of formulas:
        !           595: \begin{small}
        !           596: \begin{verbatim}
        !           597: [1] F = m*x+b@==0 @&& 0@<=x @&& x@<100;
        !           598: (m*x+b @== 0) @&& (-x @<= 0) @&& (x-100 @< 0)
        !           599: [2] all(x,F @impl x@<50);
        !           600: all(x,((m*x+b @== 0) @&& (-x @<= 0) @&& (x-100 @< 0) @impl x-50 @< 0))
        !           601: [3] ex([x,m],F);
        !           602: ex(x,ex(m,(m*x+b @== 0) @&& (-x @<= 0) @&& (x-100 @< 0)))
        !           603: [4] all(@@);
        !           604: all(b,ex(x,ex(m,(m*x+b @== 0) @&& (-x @<= 0) @&& (x-100 @< 0))))
        !           605: \end{verbatim}
        !           606: \end{small}
        !           607: In atomic formulas, all right hand sides are subtracted to the left
        !           608: hand sides at the parsing stage. Notice that the quantifier operators
        !           609: accept also lists of variables. If no variables at all are given, the
        !           610: existential or universal closure of the formula is constructed resp.,
        !           611: i.e., all free variables are quantified.
        !           612: \subsection{Functions for formulas}
        !           613: \begin{description}
        !           614: \item[simpl({\sl f})] A simplified equivalent of {\sl f}. The
        !           615: simplification strategy is described in Subsection~\ref{currentsimpl}.
        !           616: \item[qe({\sl f})] A quantifier-free formula equivalent to {\sl f}.
        !           617: The argument formulas has to obey certain degree restrictions:
        !           618: Quantified variables must not occur with a degree greater than $2$.
        !           619: Notice that with the elimination of each quantifier, the degree in the
        !           620: other variables may increase. It thus cannot be determined by
        !           621: inspection of the input whether quantifier elimination will succeed.
        !           622: \item[atnum({\sl f})] The number of atomic formulas contained in {\sl
        !           623: f}.
        !           624: \item[atl({\sl f})] The set of atomic formulas contained in {\sl f} as
        !           625: a list.
        !           626: \item[nnf({\sl f})] A negation normal form of {\sl f}. This is a
        !           627: formula equivalent to {\sl f} which contains only \verb!ex!,
        !           628: \verb!all!, \verb!@&&!, and \verb!@||! as first-order operators.
        !           629: \item[subf({\sl f},{\sl x},{\sl t})] Substitute all ocurrences of
        !           630: variable {\sl x} in formula {\sl f} by polynomial {\sl t}. This works
        !           631: for quantifier-free formulas. Quantified variables are not yet treated
        !           632: appropriately.
        !           633: \end{description}
        !           634: \end{appendix}
        !           635: \bibliographystyle{alpha}
        !           636: \bibliography{adts}
        !           637: \end{document}