GSoC 2012 Application Sachin Irukula: Implementation of Quantifiers and Cylindrical algebraic decomposition algorithm

GSoC 2012 Application Sachin Irukula: Implementation of Quantifiers and Cylindrical algebraic decomposition algorithm

Personal Details:

Name: Sachin Irukula
University: Bits-Pilani K.K.Birla Goa Campus
Email: sachin.irukula@gmail.com
IRC Username: sachin004 on freenode
GitHub Username: sachin004

Background and Skills:

I am a third year computer science undergraduate from Bits-Pilani University. I have been using C and python for programming since 2-3 years. I have been using sympy since past 3 months for implementing polynomials such as Bernstein polynomials, Laguerre polynomials, Galerkin method etc. as a part of my academic project. I have fairly good experience with numpy, scipy and wxpython. I use Fedora 16 for most of the programming purposes.

Project:

Deliverables:

Implementing quantifiers will help to deal with first and other higher order logics efficiently. Implementing cylindrical algebraic decomposition will help to do quantifier elimination from expressions and solving system of polynomial inequalities.

Description:

•Implementing quantifiers:
Universal quantifiers (∀-for all)
Existential quantifiers (∃- there exists)
Special cases of quantifiers:

1. Branching quantifier
2. Lindström quantifier
3. Mostowski Quantifiers
   •Implementing Cylindrical algebraic decomposition:
   Semi-Algebraic Sets and Cell Decomposition:
   In this CAD algorithm computes a cell decomposition of solution sets of arbitrary real polynomial systems.
   Finding cell decomposition consists of two phases:
   1.Project phase:In the projection phase, from the set of factors of the polynomial present in the quantifier free part of the polynomial system eliminate variables one by one using a projection vector. By this phase roots of the polynomials, the algebraic functions needed in the construction of the cell decomposition of the semi-algebraic set are produced.
4. Lifting phase: 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. By using the implemented CAD algorithm we will be able to use it in Quantifier elimination and solving system of polynomial inequalities.

Schedule:

•Week 1-2
Implementing Universal and Existential Quantifiers.
>>> pprint(for_all(x, a*(x ** 2)+b*x+c > 0))
\__/ a*(x**2) + b*x +c >0
\/ x
>>> pprint(exists(x, a*(x**2)+b*x+c == 0 && x>0))
_
_| (a*(x**2)+b*x+c == 0 && x>0))
_| x

•Week 3
Implementing special cases of quantifiers.

•Week 4-5
Implementing CAD for univariate polynomials
1.Implementation of Real closed fields.
2.Implementing Bernstein polynomials (Already implemented needs to be optimized).
3.Finding isolating list for the given list of polynomials

•Week 6-9
Implementing CAD for multivariate polynomials
1.Cell decomposition of solution sets of real polynomial systems which are given as input.
2.Implementing Sylvester-Habicht matrix.
3.Projection phase
4.Lifting Phase

•Week 10
Applying the implemented CAD algorithm for Quantifier elimination.
>>> qe_cad(exists(x, a*(x**2) + b*x + c =0 and a!=0))
a!=0 and 4ac-b**2 <=0

•Week 11
Applying the implemented CAD algorithm for solving system of polynomial inequalities.
>>> solve_cad(x**2+y**2 < 1, set([x,y]))
-1 < x < 1 && -sqrt(1-x**2) < y < sqrt(1-x**2)

•Week 12
Adding test cases and solvers to all the modules prepared.
Documenting the entire work completed.

Other information:

Relevant Courses done:

1. PHIL C221 SYMBOLIC LOGIC
2. CS GC363 / IS GC363 Data Structures and Algorithms
3. MATH F112 MATHEMATICS II (Linear Algebra)
   Good at programming in Python, familiarity with sympy and interested in mathematical logic (Symbolic Logic) and Algebra.
   As I have no plans or any other internship during summer I can dedicate about 45-55 hours a week for the project.
   Will be submitting pull requests every 2 weeks to keep branch merges reasonable and code reviews manageable.
   Discussion on the mailing list: https://groups.google.com/forum/#!topic/sympy/bclE0Xxl3W8

Patch Requirement:

Closed Pull requests:
https://github.com/sympy/sympy/pull/1178
Open Pull Requests:
https://github.com/sympy/sympy/pull/1156
https://github.com/sympy/sympy/pull/1179

References:

[1] http://perso.univ-rennes1.fr/marie-francoise.roy/bpr-ed2-posted2.html
[2] http://reference.wolfram.com/mathematica/tutorial/RealPolynomialSystems.html
[3] Cylindrical Algebraic Decomposition I: The Basic Algorithm" by Dennis S. Arnon, George E.Collins, Scot McCallum.
[4] Quantifier elimination and cylindrical algebraic decomposition Bob F. Caviness, Jeremy R. Johnson
[5] http://mathworld.wolfram.com/CylindricalAlgebraicDecomposition.html