Hello everyone,
My name is Damien Desfontaines, and I'm currently following a Theoretical
Computer Science Major at the École Normale Supérieure in Paris, which is one of
the most selective universities in France.
I am fairly interested in working for SymPy during the Google Summer of Code
program ; and I was looking on the website how I could use my theoretical
background to contribute in an efficient and useful way to this project. Being
really interested in formal logic, I was thinking that I may look at the Logic
module already implemented in SymPy.
So, apparently it contains the bare minimum to play around with boolean
formulas. There is also a SAT-solver, using - tell me if I am wrong - DPLL's
algorithm. So, it makes me think of several suggestions :
- Improving the SAT-solver algorithm. Many research has been done since DPLL,
and some solvers like MiniSAT are much more efficient [1].
- Implementing variants of this algorithm, for particular cases (one may want to
solve a 3-SAT instance for example, and others algorithms exists for those
particular cases - the randomized Schöning's algorithm, for example).
Variants include 2-SAT, 3-SAT, Horn-satisfiability,
XOR-satisfiability, etc [2].
- Implementing a Max-SAT-solver, and so being able to tell the maximum number of
clauses for which there exists an assignment satisfying all of them, in a set
of given clauses. Variants of this algorithm exist too, Max-{2,3}-SAT for
example. [3]
- Implementing heuristic methods, to deal with large inputs.
I would be glad to work on some of those ideas. What do you think is more useful
? I would like to have a research-oriented attitude, implementing and comparing
different algorithms doing the same task to come with the best solution
possible. So, it may be a little optimistic to apply for all of these at the
same time...
Damien Desfontaines
[1]
https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Algorithms_for_solving_SAT
http://minisat.se/
[2]
https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Complexity_and_restricted_versions
[3] https://en.wikipedia.org/wiki/Maximum_satisfiability_problem
--
You received this message because you are subscribed to the Google Groups
"sympy" group.
To post to this group, send email to sympy@googlegroups.com.
To unsubscribe from this group, send email to
sympy+unsubscr...@googlegroups.com.
For more options, visit this group at
http://groups.google.com/group/sympy?hl=en.
