GSoC 2012 Application Prateek Papriwal: Cylindrical Algebraic Decomposition - sympy/sympy GitHub Wiki
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
Email: [email protected]
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].
Deliverables
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
- CMU Sphinx(SVN Repository)
- RAXA JSS EMR(Git Repository) -- https://raxaemr.atlassian.net/wiki/display/RAXAJSS/Voice+Module+Project
References
[0] Cylindrical Algebraic Decomposition I: The Basic Algorithm" by Dennis S. Arnon, George E. Collins, Scot McCallum
[1] http://reference.wolfram.com/mathematica/tutorial/RealPolynomialSystems.html
[2] http://reference.wolfram.com/mathematica/tutorial/ConstrainedOptimizationExact.html