Cylindrical algebraic decompositions for Boolean combinations


Bradford, R., Davenport, J. H., England, M., McCallum, S. and Wilson, D., 2013. Cylindrical algebraic decompositions for Boolean combinations. In: ISSAC 2013: International Symposium on Symbolic and Algebraic Computation, 2013-06-25 - 2013-06-28. New York: ACM, pp. 125-132.

Related documents:

PDF (Author's accepted version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (4MB) | Preview

    Official URL:

    Related URLs:


    This article makes the key observation that when using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is not always the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This motivates our definition of a Truth Table Invariant CAD (TTICAD). We generalise the theory of equational constraints to design an algorithm which will efficiently construct a TTICAD for a wide class of problems, producing stronger results than when using equational constraints alone. The algorithm is implemented fully in Maple and we present promising results from experimentation.


    Item Type Conference or Workshop Items (UNSPECIFIED)
    CreatorsBradford, R., Davenport, J. H., England, M., McCallum, S. and Wilson, D.
    Related URLs
    URLURL Type
    Uncontrolled Keywordscylindrical algebraic decomposition,equational constraint
    DepartmentsFaculty of Science > Computer Science
    Publisher StatementEngland_ISSAC2013.pdf: © ACM 2013. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was publishined in 'ISSAC '13 Proceedings of the 38th international symposium on International symposium on symbolic and algebraic computation' 2013,
    ID Code33926


    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...