On the size of the tree-like resolution for the pigeonhole principle

Abstract

We improve upper and lower bounds of the size of tree-1ike resolution refutation for the pigeonhole principle. These results imply the super-polynomial separation between the size of tree-like resolution refutation and that of DAG-1ike resolution refutation. Although a stronger result was already shown for this separation, our aim is to do the separation for the pigeonhole principle, which is one of the most famous CNF formula in this field. We use a novel technique for the proof of a lower bound; we exploit the equivalence between tree-1ike resolution and the backtracking, which is a well-known algorithm for the Satisfiability.

鳩の巣原理に対する木状導出原理の証明サイズの上下限の改良を行なう.上下限の改良という本来の結果の他に, 木状導出原理による証明サイズが一般の導出原理に対するものよりも超多項式的に大きい例を, 最も研究のなされている鳩の巣原理に対しても示した.下限の証明には, 木状導出原理とSATアルゴリズムであるバックトラック法との等価性を利用した.