Hi! I would like to see that in Sage too. The combination of Gröbner bases and DPLL is very interesting (also from a verification point of view). I can only recommend to read the following paper. C. Condrat and P. Kalla, "A Groebner Basis Approach to CNF formulae Preprocessing"
I think, using PolyBoRi instead of Cocoa might improve their results ;-). Cheers, Michael --~--~---------~--~----~------------~-------~--~----~ 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 -~----------~----~----~----~------~----~------~--~---