On Saturday 17 October 2009, you wrote: > Hello Martin, Hello Minh, Hello Tom, Hello Victor, Hello William ! > > Minh, William and I just had a short conversation on #sage-devel about COQ > ( http://en.wikipedia.org/wiki/Coq ), then about SAT Solvers in Sage... > I'd be very interested in having SAT Solvers in Sage, even though I know > next to nothing about them. I would use them to solve combinatorial > problems on Graphs, as a possible alternative to linear programming. I do > not know how they compare either, but I think it's worth giving it a try. > > I was told you had all some interest in getting these solvers included in > Sage, to study combinatorics/cryptography/logic... Have you ever tried to > interface them ? My only experience with interfacing software comes from > Linear Programming, so I can not say I will be able to interface it neatly > by myself, though I'll definitely give it a thorough look. > > William mentionned mini SAT. There is a wealth of different of LP Solvers, > and I expect it to be the same for SAT Solvers. Do you all agree this is > the one we should try to get into Sage, do you have other ones you like ( > we could have to try other ones if it is too hard to include mini SAT, or > if there are license issues, etc... ). > > Thank you for your answers/comment/advices ! :-) > > Nathann
Hi Nathann, I am very interested in getting SAT-Solvers into Sage and have some prior experience with interfacing to them in the area of cryptography. You can see the results of my efforts here (which is a very simple interface): http://bitbucket.org/malb/algebraic_attacks/src/tip/anf2cnf.py Michael Brickenstein also wrote an interface which converts boolean polynomials to CNF: http://bitbucket.org/brickenstein/polybori-scripts/src/tip/cnf.py I met the (one of?) authors of cryptominisat http://planete.inrialpes.fr/~soos/CryptoMiniSat/index.html this week in Paris (who I also CCed to this e-mail). To me cryptominisat would be the ideal candidate for inclusion in Sage: 1) It is based on MiniSat which is an award winning SAT solver 2) It is tailored towards algebraic problems , e.g. it supports long XOR clauses (linear equations) better than normal SAT solvers 3) We have enthusiastic upstream support. Potential source of problems: it does not have a large user base (but it is based on a mature SAT solver) Cheers, Martin PS: Btw. I started to use your linear programming interface recently. But that is the subject of another e-mail sometime :) Thanks for working on this, everything was in place by the time I needed it. -- name: Martin Albrecht _pgp: http://pgp.mit.edu:11371/pks/lookup?op=get&search=0x8EF0DC99 _otr: 47F43D1A 5D68C36F 468BAEBA 640E8856 D7951CCF _www: http://www.informatik.uni-bremen.de/~malb _jab: martinralbre...@jabber.ccc.de --~--~---------~--~----~------------~-------~--~----~ To post to this group, send an email to sage-devel@googlegroups.com To unsubscribe from this group, send an email to sage-devel-unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/sage-devel URL: http://www.sagemath.org -~----------~----~----~----~------~----~------~--~---
