Hi, there is no canonical way of using SAT solvers in Sage yet. Incidentally, it's one of the proposals for Sage's Google Summer of Code projects. In the meantime you can use these scripts here to convert boolean polynomial systems to SAT and the solution back:
https://bitbucket.org/malb/algebraic_attacks/src/5d8dafeef675/anf2cnf.py https://bitbucket.org/malb/algebraic_attacks/src/5d8dafeef675/polybori-cnf- converter.py On Monday 16 Apr 2012, Zoresvit wrote: > So I've found the CryptoMiniSat solver implementation (optional > package)<http://trac.sagemath.org/sage_trac/ticket/418> and managed to > install it, but can't find any documentation on its' usage. Also I happend > to find some mentions about different SAT solvers interfaces integrated > into Sage but had problems with figuring out what is actually ready for > use and how it can be used. I would appreciate any help and hints on using > SAT solvers in Sage. > > Thanks. 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 email to [email protected] To unsubscribe from this group, send email to [email protected] For more options, visit this group at http://groups.google.com/group/sage-support URL: http://www.sagemath.org
