GSoC 2012 Application Prateek Papriwal: Cylindrical Algebraic Decomposition

papriwalprateek edited this page Apr 24, 2013 · 2 revisions
Clone this wiki locally

Title : Cylindrical Algebraic Decomposition

Abstract : SymPy is an open-source Python library for symbolic mathematics.Its current list of modules does not include a method for quantifier elimination and exact global Optimisation . My proposal is to bulid an effective CAD(cylindrical Decomposition algorithm) algorithm to add support for quantifier elimination and exact global optimsation . It would work as an interface for solving systems of polynomial inequalities.

Name: Prateek Papriwal


Institute : Indian Institute of Technology Delhi

IRC: prateekp on freenode

Phone: +91 9015564795

Benefits to Community

Implenting CAD algorithm will furthur help to do quantifier elimination and help in solving system of polynomial inequalities .

Quatifier Estimation is a concept of simplification used in mathematical logic,model theory and theoretical computer science . This would still furthur open new area of contributions in the field of model theory, mathematical logic etc. Quantification is one of the way of classifying formulas. Formulas with less depth of quantifier alternation are thought of as being simpler with quanifier-free formula as the simplest. Theories that have been shown decidable using quantifier elimination are-- real closed fields, boolean algebras dense linear orders, random graphs, Feature Tress .

Furthur solving system of polynomial inequalities(mathematica has this feature) would be a major plus to the Sympy. Plus furthurmore exact global optimistion can also be achived using CAD algorithm [3].


As such , the whole project is centered around the CAD(Cylindrical Decomposition Algorithm) introduced by Collins . The project would require implementation right from the scratch . As in we will be requiring development of a new module of Real Polynomial Systems. For sure, through the summer, the ideas would be discussed, modified. There might be other students working on things which are related to my project(such as Grobener Bases) and we might then share work. The Model would be very much inspired by that of Mathematica.

I would lay down rough schedule of mine. Implementation of a structured Real polynomial sytems would be of much importance . Real polynomial systems is an expression constructed with polynomial equations and inequalities combined using logical connectives and quantifiers . Below is a brief idea of implementation(it requires more illustrative explanation).

After having implemented Real polynomial systems, we would go about transforming the representation to prenex normal form . A prenex normal form consists of two parts -- Quanifiers and Quantifier free formula .

  • Semi Algebraic Sets and Cell Decomposition

CAD computes a cell decomposition of solution sets of arbitrary real polynomial systems. The objective of the original Collins algorithm was to eliminate quantifiers from a quantified real polynomial system and to produce an equivalent quantifier-free polynomial system. After finding a cell decomposition, the algorithm performed an additional step of finding an implicit representation of the semi-algebraic set in terms of polynomial equations and inequalities in the free variables.

Finding a cell decomposition of a semi-algebraic set using the CAD algorithm consists of two phases, projection and lifting.

  • The Projection Phase of CAD algorithm

In the projection phase, we will start with the set of factors of the polynomial present in the quantifier-free part of the polynomial system and eliminate variables one by one using a projection vector P. There have been several improvements which has reduced Collins projection . When there are no equations and only strict inequalities, and there are no free variables or we are interested only in the full-dimensional part of the semi-algebraic set, we can use an even smaller projection operator. For systems containing equational constraints that generate a zero-dimensional ideal, Grobner bases are used to find projection polynomials.

  • The Lifting Phase of CAD algorithm

In the lifting phase, we will find a cell decomposition of the semi-algebraic set. We will find a sample point in each of the cells and remove the cells whose sample points do not satisfy the system describing the semi-algebraic set. Next we lift the cells to cells, one dimension at a time.

After Having implemented CAD algorithm, we would use it for quantifier elimination and building an interface to solve systems of polynomial inequalities . Another application CAD algorithm "Exact Global optimisation" .(i will add more details after discussions) .Implementation of Quantifier elimination will separately require a good length description .

Description (by timeline)

April 23: Accepted student proposals announced

Community Bonding period

May 8: College major exams end.

May 21: Official "Coding Begins"

July 13: Mid-term evaluation

July 25: College classes start

August 13 : Suggested Pencils down

August 20 : Firm Pencils down

August 24: Final Evaluation deadline

My college summer schedule starts as the major exams end on 8th may(almost 13 days before the official 'coding starts' day). As soon as possible i will try to build up a structured schedule for the summer which i would follow (by discussing with the mentors or the concerned persons). My summer vacation starts almost 2 weeks before official coding day . In that period plus the community bonding period i would build up a structured schedule for the summer. I would like to be at a better off stage at midterm evaluation . So will try to finish most of my project by mid term evaluation . This would give a huge push to the project which would help in implementing more CAD application (such as Exact Global Optimsation). I will be in touch with my mentors on a daily basis and will have a solid structured schedule before the start of the first week(mentioned below).

Involvement in Open Source Organisation


[0] Cylindrical Algebraic Decomposition I: The Basic Algorithm" by Dennis S. Arnon, George E. Collins, Scot McCallum