zbMATH — the first resource for mathematics

Hard examples for resolution. (English) Zbl 0639.68093
The paper proves that there is an infinite sequence of graph-based sets of clauses of length O(n), that require resolution refutations of length at least c n, for a fixed $$c>1.$$
The author considers a sequence of graphs, obtained from the expander graphs originally defined by G. A. Margulis [Probl. Inf. Transm. 9, 325-332 (1973); translated from Probl. Peredachi Inf. 9, No.4, 71-80 (1973; Zbl 0312.22011)]. Then he defines the set of clauses by the use of these graphs. The lower bound is proved by the technique first used by A. Haken [Theor. Comput. Sci. 39, 297-308 (1985; Zbl 0586.03010)], who studied the “pigeonhole” clauses.
The study of graph-based clauses by the use of Haken’s method, enables the author to improve on the results concerning the length of minimal refutations of contradictory sets of clauses, in several respects. So, the lower bound is the best possible, except for the choice of the constant c. Then the author proves that his set of clauses has a refutation of length O(n 4) in Kleene’s axiomatic system for propositional calculus. The “pigeonhole” clauses are not known to have short (polynomial-length) proofs in a standard axiomatic system for the propositional calculus. And last, the author observes how the proof can be modified, to show an exponential lower bound for resolution refutations for sets of clauses in which each clause contains three literals (the “pigeonhole” clauses contain clauses of length n).
Reviewer: E.Savin

MSC:
 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 03B35 Mechanization of proofs and logical operations 68Q25 Analysis of algorithms and problem complexity
Full Text: