Hi [sage-devel] and [cryptominisat-devel], I finally sat (ha!) down and implemented a C++ interface between Sage and CryptoMiniSat.
For [sage-devel]: CryptoMiniSat is a SAT solver which was originally forked from MiniSat2. I chose it because (a) it's a good solver (b) it supports XOR constraints (in crypto XORs are plenty), (c) it has a good C++ API and (d) I am friends with the main developer Mate Soos. For [cryptominisat-devel]: Sage is a big open-source mathematics software package which aims to produce a viable alternative to Mathematica, Magma, Maple and Matlab. Sage uses and ships many other open-source mathematics software packages. For a while now we have been talking about including a SAT solver as an optional package. Among other things, it was one of the projects with proposed for the Google Summer of Code, but it wasn't among the three projects that we ended up choosing. Anyway, the interface works for fire-and-forget style SAT-solving. sage: frrom sage.sat.solvers.cryptominisat.cryptominisat import CryptoMiniSat sage: CMS = CryptoMiniSat() We use DIMACS-style tuples for input: sage: CMS.add_clause((1,2,3)) sage: CMS.add_clause((1,2,-3)) sage: CMS.add_clause((1,-2,3)) sage: CMS() (True, True, True) I also implemented getting learnt clauses out, because that's what I was interested in and also copy'n'pasted PolyBoRi's ANF to CNF conversion (and back), so we can do the following. We construct one round of small-scale 64-bit AES: sage: sr = mq.SR(1,4,4,4,gf2=True,polybori=True) and construct a polynomial system for it: sage: F,s = sr.polynomial_system() I implemented solving and learning, i.e., we use the SAT solver to learn new 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 btw. by default length three clauses are returned Of course, the idea is now to check whether a seesaw strategy is promising, i.e., we run the SAT solver for a while to learn new polynomials and then run a GB computation up to some limited degree to learn some polynomials, then the SAT solver again etc. Might be a stupid idea but we now have the technology to check :) Getting back tot he point: a lot is missing: documentation, XOR clause support, conflict clauses, proper SolverConf support ... Help very much appreciated. 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 Cheers, Martin PS: @Mate why does get_unitary_leants() a vector<Lit> instead of a vec<Lit>? 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? -- 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
