WWW.THESIS.XLIBX.INFO
FREE ELECTRONIC LIBRARY - Thesis, documentation, books
 
<< HOME
CONTACTS



Pages:   || 2 | 3 | 4 | 5 |

«Cylindrical Algebraic Sub-Decompositions D. J. Wilson · R. J. Bradford · J. H. Davenport · M. England Received: 22 October 2013 / Revised: 4 April ...»

-- [ Page 1 ] --

Math.Comput.Sci. (2014) 8:263–288

Mathematics in Computer Science

DOI 10.1007/s11786-014-0191-z

Cylindrical Algebraic Sub-Decompositions

D. J. Wilson · R. J. Bradford ·

J. H. Davenport · M. England

Received: 22 October 2013 / Revised: 4 April 2014 / Accepted: 13 April 2014 / Published online: 13 June 2014

© The Author(s) 2014. This article is published with open access at Springerlink.com

Abstract

Cylindrical algebraic decompositions (CADs) are a key tool in real algebraic geometry, used primarily for eliminating quantifiers over the reals and studying semi-algebraic sets. In this paper we introduce cylindrical algebraic sub-decompositions (sub-CADs), which are subsets of CADs containing all the information needed to specify a solution for a given problem. We define two new types of sub-CAD: variety sub-CADs which are those cells in a CAD lying on a designated variety; and layered sub-CADs which have only those cells of dimension higher than a specified value. We present algorithms to produce these and describe how the two approaches may be combined with each other and the recent theory of truth-table invariant CAD. We give a complexity analysis showing that these techniques can offer substantial theoretical savings, which is supported by experimentation using an implementation in Maple.

Keywords Cylindrical algebraic decomposition · Real algebraic geometry · Equational constraints · Symbolic computation · Computer algebra Mathematics Subject Classification (2010) 68W30 (Symbolic Computation and Algebraic Computation) D. J. Wilson · R. J. Bradford · J. H. Davenport · M. England (B) Department of Computer Science, University of Bath, Bath BA2 7AY, UK e-mail: M.England@bath.ac.uk D. J. Wilson e-mail: D.J.Wilson@bath.ac.uk R. J. Bradford e-mail: R.J.Bradford@bath.ac.uk J. H. Davenport e-mail: J.H.Davenport@bath.ac.uk 264 D. J. Wilson et al.

1 Introduction

1.1 Motivation A cylindrical algebraic decomposition (CAD) is a decomposition of Rn into cells arranged cylindrically (meaning the projections of any pair of cells onto the first k coordinates are either equal or disjoint) each of which is a semialgebraic set (and so may be described by polynomial relations). They are traditionally produced sign-invariant with respect to a list of polynomials meaning each polynomial has constant sign on each cell. CAD was introduced by Collins [17], and has become a key tool in real algebraic geometry for studying semi-algebraic sets and eliminating quantifiers over the reals. Other applications include robot motion planning [38], parametric optimisation [27], epidemic modelling [12], theorem proving [36] and programming with complex functions [21].

CAD usually produces far more information than required to solve the underlying problem. Often a problem will be represented by a formula and we thus require a CAD such that the formula has constant truth value on each cell.

This can be achieved by building a CAD sign-invariant for the polynomials in the formula, but that may introduce cell divisions not relevant to the formula itself. Many techniques have been developed to try and mitigate this, some of which we discuss later. However, even then algorithms may produce thousands of superfluous cells which are not part of the solution set. The key focus of this paper is the development of methods to return a subset of a CAD sufficient to solve a given problem. We show that such subsets can often be identified from the structure of the problem, motivating the following new definitions.

Definition 1 Let D be a CAD of Rn (represented as a set of cells). Then a subset E ⊆ D is a cylindrical algebraic sub-decomposition (sub-CAD).

Let F ⊂ Q[x1,..., xn ]. If D is a sign-invariant CAD for F then E is a sign-invariant sub-CAD. We define sub-CADs with other invariance properties in an analogous manner, such as truth-invariance for a Tarski formula ϕ(x1,..., xn ). If D is a truth-invariant CAD for ϕ and E contains all cells of where ϕ is satisfied then we say that E is a ϕ-sufficient sub-CAD.

As an example of when sub-CADs may be applicable, consider quantifier elimination, the original motivation for CAD. Given a quantified formula ϕ we want to derive an equivalent quantifier-free formula. For a formula over the reals this is achieved by constructing a sign-invariant CAD for the polynomials in ϕ and testing the truth of ϕ at a sample point of each cell. This is sufficient to draw a conclusion for the whole cell due to sign-invariance and thus an equivalent quantifier free formula can be created from the algebraic description of the cells on which ϕ is true.

Such an application makes no use of the cells on which ϕ is false and so a ϕ-sufficient sub-CAD is appropriate.

Of course, for a given problem we would like the smallest possible ϕ-sufficient sub-CAD. It is not usually possible to pre-identify this, but we have developed techniques which restrict the output of the CAD algorithm to provide subCADs sufficient for certain general classes of problems. These will offer savings on any subsequent computations on the cells (such as evaluating polynomials or formulae) and in some cases also offer substantial savings in the CAD construction itself. We will introduce these techniques and demonstrate how they can be combined with each other and additional existing CAD theory, but first remind the reader of the necessary background theory.





1.2 Background to CAD

Collins’ original algorithm is described in [1]. While there have been many improvements and refinements to this algorithm the structure has remained largely the same. In the first phase, projection, a projection operator is repeatedly applied to a set of polynomials, each time producing another set in one fewer variables. Together these sets contain the projection polynomials. These are then used in the second phase, lifting, to build the CAD incrementally. First R is decomposed into cells: points corresponding to the real roots of the univariate polynomials, and the open intervals defined by them. Then R2 is decomposed by repeating this process over each cell using the bivariate polynomials (evaluated at a sample point). The output for each cell consists of sections (where a polynomial Cylindrical Algebraic Sub-Decompositions 265 vanishes) and sectors (the regions between). Together these form a stack over the cell, and taking the union of these stacks gives the CAD of R2. This is repeated until a CAD of Rn is produced. To conclude that the CAD is sign-invariant we need delineability. A polynomial is delineable over a cell if the portion of its zero set over that cell consists of disjoint sections. Then a set of polynomials is delineable over a cell if each is delineable and the sections of different polynomials over the cell are either identical or disjoint. The projection operator used must ensure that over each cell of a sign-invariant CAD for the projection polynomials in r variables, the polynomials in r + 1 variables are delineable.

All cells include a cell index and a sample point. The index is an n-tuple of positive integers that corresponds to the location of the cell relative to the rest of the CAD. Cells are numbered in each stack during the lifting stage (from most negative to most positive), with sectors having odd numbers and sections having even numbers. Therefore the dimension of a given cell can be easily determined from its index: simply the number of odd indices in the n-tuple.

Our algorithms in this paper will produce sub-CADs that are index-consistent, meaning a cell in a sub-CAD will have the same index as it would in the full CAD. Further, we will assume that cells are stored lexicographically by index.

Important developments to CAD include: refinements to the projection operator [7,28,33], reducing the number of projection polynomials and hence cells; partial CAD [18], where the structure of the input formula is used to simplify the lifting stage; the theories of equational constraints and truth-table invariance [4,34] where the presence of equalities in the input further refines the projection operator; the use of certified numerics in the lifting phase [29,41]; and CAD via triangular decomposition [16] which constructs a decomposition of complex space and refines this to a CAD.

Constructing a CAD is doubly exponential in the number of variables [22]. While none of the improvements described above (or introduced in this paper) circumvent this they do make a great impact on the practicality of using CAD. Note that CAD can depend heavily on the variable ordering used (from linear to doubly-exponential [11]). In this paper we work with polynomials in Q[x] with the variables x = x1,..., xn in ascending order (so we first project with respect to xn and continue until we reach univariate polynomials in x1 ). The main variable of a polynomial (mvar) is the greatest variable present with respect to the ordering. Heuristics to assist with selecting a variable ordering (and other choices) were discussed in [6,23] and are equally applicable to sub-CADs.

1.3 New Contributions

In Sect. 2 we present new algorithms to produce sub-CADs, as well as surveying the literature to identify other examples of sub-CADs. To the best of our knowledge the concept of a sub-CAD has never been formalised and unified before.

We start in Sect. 2.1 by defining a Variety sub-CAD (V-sub-CAD). This idea combines the ideas of: equational constraints [34], where the presence of an equation implied by the input formula improves the projection operator;

and partial CAD [18], where the logical structure of the input allows one to truncate the lifting process when the truth value can already be ascertained. We observe that if the input formula contains an equational constraint then all valid cells must lie on the variety it defines and hence it is unnecessary to produce cells not on this variety.

In Sect. 2.2 we define a Layered sub-CAD (L-sub-CAD) as the cells in a CAD of a specific dimension or higher. It has been noted previously that a problem involving only strict inequalities would require only the cells in a CAD of full-dimension [31,40]. We generalise this idea and explain when it may be of use, for example to solve problems whose solution sets are of known dimension or in applications like robot motion planning where only cells of certain dimensions are of use.

These new ideas improve the practicality of using CAD and their effect can be increased by combining them, as discussed in Sect. 3.1. For example, consider formulae of the form f = 0 ∧ ϕ where ϕ involves only strict inequalities. Then a Layered Variety sub-CAD (LV-sub-CAD) can provide the cells of full dimension on the variety and thus the generic families of solutions.

266 D. J. Wilson et al.

These new ideas may also be combined with many existing aspects of CAD theory. It is of course sensible to combine the restricted output of a variety CAD with the theory of reduced projection with respect to an equational constraint. However, it is also possible to combine with the projection operator for truth-table invariant CAD (TTICAD) recently presented in [4]. A TTICAD is one for which each cell is truth invariant for a list of formulae, utilising equational constraints in the individual formulae to reduce the number of projection polynomials. We discuss when and how truth-table-invariant sub-CADs can be produced in Sect. 3.2. In Sect. 5.2 we examine a problem where a LV-sub-TTICAD can be used to identify almost all the solutions (the set of missing solutions has measure zero). This approach produces 88 % fewer cells than using TTICAD alone and takes seconds rather than minutes (while trying to tackle the problem with a traditional CAD is infeasible). This and two other case studies demonstrating the benefit of the new algorithms are presented in Sect. 5.

In Sect. 4 we give a complexity analysis of certain sub-CADs. Although none of the new theory allows us to avoid the doubly exponential nature of CAD they do allow for improved asymptotic bounds. The improvement is n n−1 a drop in the constant term of the double exponent, and we note that 22 = O(22 ) so such savings can have a substantial effect. This is reflected by experimental results in Sect. 5 where substantial increases in efficiency due to sub-CAD technology are demonstrated.

2 Sub-CADs

We aim to return only those cells necessary to solve the problem at hand: a φ-sufficient sub-CAD. However, trying to identify the minimal φ-sufficient sub-CAD for a problem would mean essentially solving the problem itself and so we instead explain how to identify sets of valid or invalid cells during the lifting stage at minimal cost. Indeed, the two new approaches to sub-CAD we present require only simple checks on cell-dimensions (easily obtained via the cell-index). We present theory and algorithms for variety and layered sub-CADs in Sects. 2.1 and 2.2, and then in Sect. 2.3 we put our work into context by surveying the CAD literature for relevance to sub-CADs.

2.1 Variety Sub-CADs

Recall the definition of an equational constraint.

Definition 2 Let ϕ be a Tarski formula. An equational constraint is an equation, f = 0, logically implied by ϕ.

Equational constraints may be given explicitly (as in f = 0∧φ), or implicitly (as f 1 f 2 = 0 is in ( f 1 = 0∧φ1 )∨( f 2 = 0∧φ2 )). The presence of an equational constraint can be utilised in the first projection stage by refining the projection operator [34] and also in the final lifting stage by reducing the amount of polynomials used to construct the stacks [25]. If more than one equational constraint is present then further savings may be possible [13,35]. We restrict ourselves to a single equational constraint, and if multiple equational constraints are present we assume that one has been designated.

Definition 3 Let ϕ be a Tarski formula with equational constraint f = 0. A truth-invariant sub-CAD for ϕ consisting only of cells lying in the variety defined by f = 0 is a Variety sub-CAD (V-sub-CAD).



Pages:   || 2 | 3 | 4 | 5 |


Similar works:

«Search now 4r70w Transmission Rebuild Manual PDF is free to download. Get 4r70w Transmission Rebuild Manual Book to read online 4R70W TRANSMISSION REBUILD MANUAL PDF Download: 4R70W TRANSMISSION REBUILD MANUAL PDF Digital document 4R70W TRANSMISSION REBUILD MANUAL File update. So you are person who likes to download 4r70w transmission rebuild manual Pdf to any kind of device,whether its your laptop, Kindle or iPhone, there are more options now than ever before. Perhaps because of the growing...»

«Th e N ec es s it y o f R e f o r mi n g th e C hu r ch John Calvin (1509-1564) To The Most Invincible Emperor Charles V., And The Most Illustrious Princes And Other Orders, Now Holding A Diet Of The Empire At Spires, !1543 A HUMBLE EXHORTATION Seriously to Undertake The Task Of Restoring The Church. Presented In The Name Of All Those Who Wish Christ To Reign. August Emperor, You have summoned this Diet, that, in concert with the Most Illustrious Princes and other Orders of the Empire, you may...»

«dok-line AFRIKA Annotierte Online–Bibliographie 26. März 2013 ISSN: 1611-1109 2013 / 1 Herausgeber: GIGA German Institute of Global and Area Studies GIGA Informationszentrum Neuer Jungfernstieg 21 • 20354 Hamburg • Tel.: (040) 42825-598 • Fax: (040) 42825-512 E-Mail: info@giga-hamburg.de • Web: www.giga-hamburg.de/iz Christine Hoffendahl / Anne Jansen ECOWAS und die Lösung gewaltsamer Konflikte in Westafrika ECOWAS and the solution of violent conflicts in West Africa This short...»

«falcon schuhe falcon schuhe Schuhe bei Sarenza Neue Kollektion bei Sarenza.de. Neue Kollektion bei Sarenza.de. Gratis Versand nach DE AT. Schuhe von Top Marken Riesen Auswahl an tollen Schuhe. Riesen Auswahl an tollen Schuhe. Mode  Fashion online entdecken! Görz17 + 0 Versand Görtz 17 im GÖRTZ Online-Shop. Görtz 17 im GÖRTZ Online-Shop. Kostenloser Versand Rückversand! Ecco Die neue Kollektion ist da! Die neue Kollektion ist da! Gratis Versand, jetzt online kaufen www.rosebikes.de...»

«Moving TFS to a Cloud Cadence Buck Hodges, Valentina Keremidarska August 20, 2012 (v. 1.3) Introduction Until the TFS 2012 product cycle, the TFS team had followed the divisional approach of milestones and shipping only a boxed product. Two things changed with TFS 2012. First, we made a decision at the beginning of the cycle to adopt Scrum. Second, we deployed tfspreview.com in April, 2011 and began the transformation to an online service team that also ships an on-premises server product that...»

«See discussions, stats, and author profiles for this publication at: https://www.researchgate.net/publication/265172026 MILITARY LEADERSHIP AND THE CULTIVATION OF WISDOM Conference Paper · November 2011 DOI: 10.13140/2.1.4973.5045 READS 2 authors: Emmet Mcelhatton Brad Jackson Victoria University of Wellington 6 PUBLICATIONS 6 CITATIONS 33 PUBLICATIONS 450 CITATIONS SEE PROFILE SEE PROFILE All in-text references underlined in blue are linked to publications on ResearchGate,...»

«PART B VANGUARD® BOND INDEX FUNDS STATEMENT OF ADDITIONAL INFORMATION April 26, 2016 This Statement of Additional Information is not a prospectus but should be read in conjunction with a Fund’s current prospectus (dated April 26, 2016). To obtain, without charge, a prospectus or the most recent Annual Report to Shareholders, which contains the Fund’s financial statements as hereby incorporated by reference, please contact The Vanguard Group, Inc. (Vanguard). Phone: Investor Information...»

«Driven by Desperation Transactional Sex as a Survival Strategy in Port-au-Prince IDP Camps May 2011 Table of Contents I. ACKNOWLDEGEMENTS II. EXECUTIVE SUMMARY III. METHODOLOGY INTRODUCTION A. SAMPLING METHODOLOGY B. FOCUS GROUP METHODOLOGY C. IV. BACKGROUND AND INTRODUCTION COUNTRY CONTEXT A. B. GENDER INEQUALITY AND SEXUAL GENDER BASED VIOLENCE C. FOOD INSECURITY V. KEY FINDINGS, OBSERVATIONS AND TESTIMONIES A. KEY FINDINGS B. TRANSACTIONAL SEX C. SEXUAL VIOLENCE SURROUNDING THE TRANSACTION...»

«Optimality Theory Chapter 6 93 6. Syllable Structure Typology I: the CV Theory 6.1 The Jakobson Typology It is well-known that every language admits consonant-initial syllables.CV~., and that some languages allow no others; that every language admits open syllables.~V. and that some admit only those. Jakobson puts it this way: “There are languages lacking syllables with initial vowels and/or syllables with final consonants, but there are no languages devoid of syllables with initial...»

«Whole Grain Connection A California non-profit corporation, 501 (c) 3 500 W. Middlefield Road #2 Telephone: 650 938 2865 Mountain View www.sustainablegrains.org California 94043 e-mail: barmbaker@aol.com Aiming to enhance the desirability and availability of 100% whole grain breads, and other 100% whole grain products, from organically and sustainably grown grains, and thereby connecting farmers and bakers. Catalog of Wheat Seeds & Books Seed Program The Whole Grain Connection wheat seed...»

«BEYOND TORT: COMPENSATING VICTIMS OF ENVIRONMENTAL TOXIC INJURY ALBERT C. LIN* ABSTRACT Environmental toxic tort cases often pose difficult problems of proof. A substance’s toxicity may be unknown or uncertain. A combination of factors may cause a plaintiff’s injury, and the injury may arise many years after a plaintiff’s exposure to a toxic substance. On the one hand, some plaintiffs, particularly those with “signature” illnesses or whose illnesses occur as a cluster of cases, may be...»

«Postmodern Doubts and Theological Education (Part 1) By Bob Wilkin Postmodern Agnosticism Rules at Most Conservative Theological Institutions Most Evangelicals have no idea what is being taught in Christian colleges and seminaries in America today. They assume that those training for the ministry are being taught the Bible, sound doctrine, and how to teach and preach. The truth is hard to believe. The norm in most American theological institutions, among both the faculty and the students, is...»





 
<<  HOME   |    CONTACTS
2016 www.thesis.xlibx.info - Thesis, documentation, books

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.