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 Po
Hi,
> > Minh, William and I just had a short conversation on #sage-devel about COQ
> > ( http://en.wikipedia.org/wiki/Coq ), then about SAT Solvers in Sage...
I just want to mention that on the contrary to what has been said on irc, the
primary goal of Coq is not to automatically prove t
On Saturday 17 October 2009, you wrote:
> Hello Martin, Hello Minh, Hello Tom, Hello Victor, Hello William !
>
> Minh, William and I just had a short conversation on #sage-devel about COQ
> ( http://en.wikipedia.org/wiki/Coq ), then about SAT Solvers in Sage...
> I'd be very interested in havin
