Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleUsing the Groebner basis algorithm to find proofs of unsatisfiability
Author(s) Matthew Clegg, Jeffery Edmonds, Russell Impagliazzo
TypeArticle in Conference Proceedings
AbstractA propositional proof system can be viewed as a non-deterministic
algorithm for the (co-NP complete) unsatisfiability problem.
Many such proof systems, such as resolution, are also used as
the basis for heuristics which deterministically search for short
proofs in the system.
We discuss a propositional proof system based on algebraic reasoning,
which we call the Groebner proof system because of a tight
connection to the Groebner basis algorithm. For an appropriate
measure of proof size, we show that (a degree-limited implementation
of) the Groebner basis algorithm finds a Groebner proof of a
tautology in time polynomial in the size of the smallest such proof,
In other words, unlike most proof systems, the non-deterministic
algorithm can be converted to a deterministic one without loss in
We then compare the power of the Groebner proof system to
more studied systems. We show that the Groebner system polynomially
simulates Horn clause resolution, quasi-polynomially simulates
URL http://doi.acm.org/10.1145/237814.237860
Translation No
Refereed No