Hi Mate, On Monday 04 Jun 2012, Mate Soos wrote: > > clauses which we then translate into polynomials: > > sage: from sage.sat.boolean_polynomials import solve, learn > > sage: H = learn(F, s_verbosity=3, s_max_restarts=1000) > > sage: H > > Polynomial Sequence with 167 Polynomials in 126 Variables > > sage: H.ideal().interreduced_basis() > > Polynomial Sequence with 149 Polynomials in 126 Variables > > All I can say is: beautiful! Very-very good work! We should have done > this years ago.
Especially since it was so easy! > > Getting back to the point: a lot is missing: documentation, XOR clause > > support, conflict clauses, proper SolverConf support ... Help very much > > appreciated. > > I'll take a look and try to get some of these done. None should be very > difficult. Agreed, better ANF to CNF conversion (and back) might be the hardest nut to crack. Currently, I am only supporting very sparse polynomials because I use PolyBoRi's conversion which is "essentially" truth table based (but with some minimisations). This whole cutting XOR chains business etc. needs to be added for polynomials with many variables. Or shall we wrap your anfconv code? > > I am tracking the interface code and the scripts to install CryptoMiniSat > > in Sage on bitbucket: > > > > Interface: https://bitbucket.org/malb/sage-cryptominisat > > SPKG: https://bitbucket.org/malb/cryptominisat-spkg > > > > See also http://trac.sagemath.org/sage_trac/ticket/418 > > Thanks, I'll work on them from there. Note I'll be travelling this week (Kaiserslautern, for a workshop on linear algebra in GB computations), so I won't be working much on this. > > PPS: @Mate why do you install stdint.h in Makefile.am? It seems it's only > > relevant on Windows where Makefile.am shouldn't be used? > > Fixed also in that branch. Also, I have now moved all include files > from 'blah/include' to under 'blah/include/cryptominisat/' so when you > have to use '#include "cryptominisat/Solver.h"' for example. I hope you > agree it's much better this way. I have also fixed some other, misc > things in the makefile. Sounds good :) Cheers, Martin -- name: Martin Albrecht _pgp: http://pgp.mit.edu:11371/pks/lookup?op=get&search=0x8EF0DC99 _otr: 47F43D1A 5D68C36F 468BAEBA 640E8856 D7951CCF _www: http://martinralbrecht.wordpress.com/ _jab: [email protected] -- To post to this group, send an email to [email protected] To unsubscribe from this group, send an email to [email protected] For more options, visit this group at http://groups.google.com/group/sage-devel URL: http://www.sagemath.org
