Using the Groebner basis algorithm to find proofs of unsatisfiability
Matthew Clegg, Jeffery Edmonds, Russell Impagliazzo · 1996
A propositionalproof system can be viewed as a non-deterministic algorithm for the (co-NP complete) unsatisfiabilit y problem.Many such proof systems, such as resolution, are rdso used as the basis for heuristics which deterministicrdly search for short proofs in the system.We discuss a propositional proof system baaed on algebraic rea soning, 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 implement =ation 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, urdike most proof systems, the non-deterministic algorithm can be converted to a deterministic one without loss in power.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 tree-like resolution, and weakly exponentially simulates resolution.Thus, Groebnerproofs will have better than worst-case behaviour on the same classes of inputs that resolution does.On the other hand, there are simple tautologies which have polynomialsize Groebner proofs but which require exponential-size resolution proofs.We also compare the Groebner proof system to the similar Nullstellensatz proof system introduced in [BIK+94].We show a family of tautologies that have degree 3 (and hence polynomirdsize) Groebner refutations, but which require @(W degree Nullst ellensat z refutations.Thus, there is an exponential separation between the two systems.These results suggest that the Groebner basis algorithm might replace mmlutian M s bseie far hem.ieticsfar NP.emnple&e pmh