Hi Damien,
The problem is that SymPy likely cannot (and most probably should not)
try to compete with the state of the art (e.g., the DPLL implementation
that I put in will never reach the speed of MiniSAT and other solvers out
there). That said, if there is a need within SymPy to have some form of
inference (which was the case for SAT solving in order to do assumptions),
then there is merit in rolling our own solver for it.
So I would suggest trying to find some reasoning task that you're
interested in and can also contribute to some other part of SymPy (MaxSAT
or partial weighted MaxSAT very well may fit the bill, but I do not see the
connection just yet).
Cheers,
Christian
On Fri, Mar 23, 2012 at 11:35 AM, Damien Desfontaines <ddfontai...@gmail.com
> wrote:
> 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.
>
>
--
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.
