Using the Groebner basis algorithm to find proofs of unsatisnability

Abstract

A 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 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, Groebner proofs 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 polynomialsize) Groebner refutations, but which require Θ(√n) degree Nullstellensatz refutations. Thus, there is an exponential separation between the two systems. These results suggest that the Groebner basis algorithm might replace resolution as a basis for beuristics for NP-complate problems. We have done some preliminary experiments comparing [CW]'s implementation of the Groebner basis algorithm to [KS]'s implementation of the Putnam-Davis procedure for unsatisfiability. [KS]'s program is superior on the instances tested. However, the difference is small enough to hope that further optimization of the Groebner basis algorithm for unsatisfiability could make it the method of choice.