Mate Soos’ CryptoMiniSat won the SATRace 2010. Congratulations Mate! For those who don’t know CryptoMiniSat, it is a fork of MiniSat which supports XOR clauses (Gaussian elimination!) among other things. This makes it particularly suitable for cryptographic problems. I’ll try to make an optional Sage Package for CryptoMiniSat soon-ish.
Thanks!
I think I will finally improve anf2cnf.py in the coming weeks: I need it dearly. I wrote a generic stream cipher problem generator in Sage in only one night… I was completely blown away, I must say. It took me _months_ to write the same in C++.
Small-ish comment: I can easily make “mq.MPolynomialSystem(L+s).eliminate_linear_variables(maxlength=1)” take a minute or more with relatively simple problem ciphers :S I will get back to you on this.