数理解析研究所講究録1120 巻 1999 年 51-57

51

鳩の巣原理に対する挙状導出原理の証明サイズの上下限の改良
Improved Upper and Lower Bounds of the Size of Tree-Like Resolution
for the Pigeonhole Principle
宮崎修–

岩間 -雄

Shuichi MIYAZAKI

Kazuo IWAMA

京都大学大学院情報学研究科〒 606-8501 京都市左京区吉田本町{shuichi,}$\mathrm{i}_{\mathrm{W}\mathrm{a}\mathrm{m}}\mathrm{a}$$@\mathrm{k}\mathrm{u}\mathrm{i}\mathrm{s}$. kyoto-u. . jp$\mathrm{a}\mathrm{c}$

摘要: 鳩の巣原理に対する木町導出原理の証明サイズの上下限の改良を行なう. 上限は従来の$O(n^{3}n!)$ を $O(n^{2}n!)$ に, 下限は従来のをに改良する. 本結果にはり, 鳩の巣原理に$2^{n}$$( \frac{n}{4\log^{2}n})^{n}$

対する網状導出原理の証明サイズが–般の導出原理の証明サイズの多項式では抑えられないことが導かれる. 下限の証明には, バックトラック法と木状導出原理の関係を利用するという, これまでにない新たな手法を用いた.
キーワード: 導出原理, 木状導出原理, 鳩の巣原理

1

はじめに

Bonet らは, 一般の導出原理では多項式サイズで証明できるが, 木状導れたのはごく最近である [2].

証明系とは, 和積形論理式の充足不能性を証明するための非決定性の手続きであり, 多項式時間で計算可能な規則を適用していくことにより充足不能性を証明する. 従って, 全ての充足不能論理式に対して多項式時間で動作する証明系が存在すればとなる [5]. しかし,であることが強く予想されているため, 証明系に対する証
明サイズの指数下限を証明するという研究は盛んに行なわれてきた. それでもなお, Frege システム
[3] のように, 未だ指数下限が示されていない証明系は数多く存在する.
導出原理は最も基本的な証明系であり, 1985 年に Haken により初めて証明サイズの指数下限が示された. Haken は鳩の巣原理を書き下した論理式を用いて指数下限を証明したのであるが, 彼の証明は難しい手法を使っており, 理解が困難であった.
そのため, その後も多くの研究者達が, より簡単な証明を求めて研究を進めている [1, 4, 8].
木状導出原理は, 証明が–般の有向非循環グラフ
でなく, 木に制限された導出原理である. 証明サイズの観点からは, 環状導出原理の方が–般の導出原
理よりも指数的に弱いというのが直観的な常識である. しかし, それにも関わらず; そのことが証明さ$\mathrm{N}\mathrm{p}_{=\mathrm{C}}\mathrm{o}\mathrm{N}\mathrm{p}$$\mathrm{N}\mathrm{P}\neq \mathrm{c}\mathrm{o}\mathrm{N}\mathrm{P}$

出原理ではある$\epsilon$に対して$2^{\Omega(n^{\epsilon})}$ステップかかってしまう論理式の例を示した [2].
本論文では, 上述と同様の分離を鳩の巣原理に対して行なう. 鳩の巣原理に対する –般の導出原理の証明サイズの上限と木状導出原理の証明サイズの下限は, これまで $O(n^{3}2^{n})$ および$2^{n}$であったため[4], 上記の分離を行なうことはできなかった. 本論
文では下限をに改良する. これにより,$( \frac{n}{4\log^{2}n})^{n}$

鳩の巣原理に対する木状導出原理の証明サイズが,一般の導出原理の最短証明サイズの多項式では抑えられないことが分かる. また, 上限に対してもわず
かながら改良を行なった.
本論文では, 下限の証明に, バックトラック法と木状導出原理の等価性を利用している. この等価性は–般には認識されていたが, その有効性はこれまで認められていなかった. 本論文では, バックト

ラック法を使って木状導出原理の証明サイズの解析を行なうことにより, これまでより大きな下限を出すことができた.

本稿の構成は以下の通りである. 2 節では, 導出
原理, バックトラック法 および, 鳩の巣原理に対する基本的な定義を行なう. また, 上述した導出原

理とバックトラック法の関係についても述べる. 3

52

節では鳩の巣原理に対する木状導出原理の証明サイ
ズの下限

4 節では鳩の巣原理にす.

$( \frac{n}{4\log^{2}n})^{n}\not\in_{J}\overline{\mathrm{T}\backslash }$対する –般の導出原理の証明サイズの上限$O(n^{2}2^{n})$を示し, これを用いて罪状導出原理の証明サイズの上限 $O(n^{2}n!)$ を示す. これら上下限に対する議論
は, 一般化された鳩の巣原理 ( $n+1$ 対 に限ら$n$ず, $m$ 対 $n(m>n)$ の場合) に対しても成り立つ
ことに注意されたい. 最後に, 5 節で今後の研究課
題について述べる.

2

導出原理および鳩の巣原理

導出原理による証明は有向非循環グラフにより
この有向非表すこともできる (例えば [9] 参照).

循環グラフが木であるとき, 証明は木状であるといい, この木を証明木という. 以下に, 証明木の形式的な定義を行なう. 充足不能論理式 $f$ に対する導出
原理の証明木とは根付き二分木のことである. 証明
木の各頂点 には項が対応しており, これを $Cl(v)$がと書く. $Cl(v)$ は以下の条件を満たしている.
$f$は中の項であり, 葉でない場合
葉のとき, $Cl(v)$は 2 つの項 $Cl(v_{1})$ と $Cl(v_{2})$ から導出された項であはとの子である. さらに,る. ただし,である. 証明木のが根のとき, $Cl(v)$ は空の項
$v$

$v$

$v$

$v$

$v_{2}$$v_{1}$$(\emptyset)$

論理変数 またはその否定房をリテラルと言い,リテラルの和を項と言う. 項の積を和馬形 (CNF)
論理式と呼ぶ. CNF 論理式 $f$ の変数にどのようにまたは 1 を割り当てても $f=1$ とできないとき,
$x$

$0$

は充足不能であると言う.
鳩の巣原理とは 要素の集合と $n+1$ 要素の集合の間に全単射がないということを述べている. $(n+$羽の鳩が 個の巣に入るとき, 必ず 2 羽以上入る巣が存在するという形で表される. ) $PHP_{n}^{n+1}$ は鳩$f$頂点数を証明木のサイズと言う.
バックトラック法 [7] とは, CNF 論理式の充足可能性問題 (SAT) に対する解法アルゴリズムの $-$
つである.

$n$

の巣原理を和判形論理式の形で書き下したものである.

$PHP_{n}^{n+1}$

は $n(n+1)$ 個の変数 $x_{i,j}(1\leq i\leq$$n+1,1\leq j\leq n)$ から成り,

が巣

$j$

に入ると考える.

$x_{i,j}=1$ のとき, 鳩(i) $(x_{i,1}+x_{i,2}+\cdots+x_{i,n})$$(1\leq$$(1\leq i\leq n+1)$ , (ii)$k\leq n$ ,1 $\leq i<j\leq n+1$ ). 従って全部で$(n+1)+ \frac{1}{2}(n^{2}(n+1))$ 項存在する.
(i) は, 各鳩が必ずどこかの巣に入ることを, (ii) は, 各巣には
高々 1 羽の鳩しか入らないことを表した項である.
(i), (ii) の条件を満たす変数割り当ては存在しないの項から出来ている.

$(\overline{x_{i,k}}+\overline{x_{j,k}})$

ため,$PHP_{n}^{n+1}$

は充足不能である.

導出原理とは充足不能論理式に対する証明系である. 導出原理は導出規則と呼ばれるただ–つの規則からなっている. 導出規則は 2 つの項 $(A+x)$ および
から新たな項 $(A+B)$ を導出する規則でおよび $B$ はリテラルの和を表す.
ある. ただしから $(A+B)$ が導出される$(A+x)$ およびとき, この導出により変数 が削除されたという.
導出原理による充足不能論理式 $f$ の証明とは項の$(B+\overline{x})$$A$$(B+\overline{x})$

$x$

列
$f$

$C_{1},$$c$$C_{2,t}\ldots,$のことである.

中の項であるか,

2 つの項$C_{/j}$ら導出された項である. また,ある.

う.

ここで, 各$C_{i}$

はと $C_{k}(j, k<i)$ か$C_{t}$

は空の項$(\emptyset)$$f$

で証明中に現れた項の数を証明のサイズと言$f$

中の変数 , および$x$を代入することによりで表す. バックトラッを簡単化した結果をん $=a$

ク法では, 適当な変数

$x$

に

$x$

に対して $f_{x=0}$ と $f_{x=1}$ を計$a$算するという手続きを再帰的に行なうアルゴリズムである. いずれかの時点で論理式が 1 に簡単化されれば $f$ は充足可能であり, 全ての葉において

$0$

とな

れば $f$ は充足不能である.

$i$は以下の 2 種類$PHP_{n}^{n+1}$$f$$a\in\{0,1\}$ に対して,

$n$

$1$

CNF 論理式 ,バックトラック法による探索の様子は, バックト

ラック木を用いて表すことができる. 充足不能論
理式 $f$ に対するバックトラック木とは, 根付き二分木であり, 以下の 3 つの条件を満たすものを言う.

(i) 頂点$v$

から二つの子への枝$e_{1}$と$e_{2}$には同じ変に対する変数代入のラベル $(x=0)$ と $(x=$1) が付いている. (ii) 任意の葉 と任意の変数は根から までの枝に高々 1 回しか現
に対して,
までの
れない. (iii) 各頂点 に対して, 根から

数

$x$

$x$

$v$

$v$

$x$

$v$

$v$

枝に現れる変数代入からなる部分割り当てを As $(v)$で表す. このとき, 各頂点 に対して が葉である
とき, 及びそのときに限り, $f$ は As $(v)$ で になる. バックトラック木の頂点数をバックトラック木のサイズと言う.
補題 1 .
を充足不能な CNF 論理式とする. もし, $f$ に対するサイズ の木割導出原理の証明木に対するサイズ 以下のバックトが存在すれば,
ラック木が存在する.
証明. $f$ に対する任意の証明木を $R$ とする. 木状導出原理の場合, 最小の証明木は, 根から葉までのどのパスにおいても同じ変数が高々 1 度しか現れ
$v$

$v$

$0$

$f$

$k$

$f$

ないことが知られている [9].

$k$

したがって, 一般性を53

失うことなく $R$ はそのような性質を持っていると仮定する.
上述の $R$ からバックトラック木 $B$ を作る.

$B$はと同型であり, この同型性により $R$ の頂点
に
$B$
$B$
対応する
の頂点を
とする. ここで,の各枝を与えれば良いことが分かる.

3

証明サイズの下限について$R$$v_{i}$$u_{i}$に以下のようにラベルを割り当てていく.
の頂点とし,$v_{i_{1}}$と物 2 を$Cl(v_{i})=(\mathrm{A}+B)$ ,$v_{i}$$v_{i}$

を $R$の子とする. さらに,$Cl(v_{i_{1}})=(A+x),$$Cl(v_{i_{2}})=$

本節では, $PHP_{n}^{n+1}$ に対する雨竜導出原理の証
明サイズの下限を与える.
$PHP_{n}^{n+1}$ に対する木状導出原理の証明
定理 1.

木のサイズは少なくとも$( \frac{n}{4\log}=_{n})^{n}$

証明.

である.

であるとする. このとき, 枝
おに, それぞれラベル $(x=0)$ および

ここでは, 簡単のため,下限を示す.
定理で述べられているへの拡張は本証明$(x=1)$ を割り当てる. このようにしてできた木 $B$

を 4 の倍数とする.
補題 1 より, $PHP_{n}^{n+1}$ に対するバックトラック木のサイズが少なくともであることを言えば良$(B+\overline{x})$よび$(u_{i}, u_{i_{1}})$$(u_{i}, u_{i_{2}})$が $f$ に対するバックトラック木であることを以下で示す.

がバックトラック木の条件 (i) および (ii) を満たすことは容易に分かる. 従って, 以下では条件(iii) が成り立つことを示すわけであるが, このために,の各浅 に対して, As $(u)$ により が になることを言う. もし,の葉以外の頂点で が
$B$

$u$

$f$

$B$

$0$

$f$

になる場合には, その頂点以下を切り捨てて, その頂点を葉にすることによりサイズを大きくせずに条件 (iii) を満たす木に変更できるため, 上述のことを示せば十分である. そのために, 「各 に対して, バックトラック木の割り当て As(u のが証明
$i$

$B$

の項 $Cl(v_{i})$ を にする. 」 という命題が成り立つことを示す. この命題が示されれば, $R$ の葉に対応する項は $f$ 中の項であることから, $B$ の馬脳に対して, As $(u)$ により $f$ が になることが言え木$( \frac{n}{4\log^{2}n})^{n}$の後に述べる.

簡単のため

$n$

$( \frac{n}{4})^{\frac{n}{4}}$

$B$

$0$

$( \frac{n}{4})^{\frac{n}{4}}$

$R$

$0$

$u$

$0$

い.

$B$

を $PHP_{n}n+1$ に対する任意のバックトラック

木とする. 前述のように, $B$ の頂点 は部分割り
当て As $(v)$ に対応している. ここで, その部分割り
当てを $(n+1)\cross n$ の行列で表すことにする. 図 1$v$

は,に対する部分割り当ての例を示していのセルは変数 $Xi,j$ に対応しており,そのセルに $0(1)$ が書き込まれている状態を, 変数に値 0(1) が割り当てられている状態と考える.
る.

$PHP_{4}^{5}$$F^{1}\mathrm{J}i$

, 行

$j$

$x_{i,j}$

例えば図
$0,$

は,

$1(\mathrm{b})$$x_{3,3}$.

$=$$x_{4,1}$$x_{1,4}=x_{2,2}=x_{4,4}=x_{5,3}=$$=$

1 という割り当てを表して従って, バックトラック木 $B$ の頂点 が葉であるための条件は, 以下の (i) または (ii) が成り立つことである. (i) As $(v)$ のある列が全て であ
いる.

$v$

$0$

る.

上記の命題を帰納法により示す. 根に対して命題が成り立つことは明らかである. 次に頂点に対して成り立つと仮定する. すなわち, 項 $Cl(v_{i})$でが割り当て Asになる, と仮定する. このとき,の子でも成り立つことを示す.
の子をとし, $Cl(v_{i})=(A+B),$ $Cl(v_{i})1=$$(A+x),$ $Cl(v_{i})2=(B+\overline{x})$ とする. このとき,$B$へのラベルの付け方から, 枝にはラベル$(x=0)$ が付けられているはずである. 従って,(ii) As$(v)$のある行に 1 が 2 つ入っている. .

る.

$v_{i}$$(u_{i})$$0$$v_{i}$$v_{i_{1}},$$v_{i}$$v_{i_{2}}$($(v_{i}, v_{i_{1}})$

As $(u_{i_{1}})=As(u_{i})\cup\{(x=0)\}$ である. 仮定より,
力領 $(A+B)$ を にするので, As
As
は項$(A+x)$ を にする. 同様の議論により, As$(u_{i})$

$0$

$0$

が $Cl(v_{i})2$ を$0$にすることも示される. 従って上記

が $f$ に対するバックトラック木
命題は示され,$B$であり,の頂点数は $R$ の頂点数以下であること$B$が示された.

ロ

上記の補題より, 木状導出原理の証明サイズの下限を与えるには, バックトラック木のサイズの下限’(b)

図 1: $PHP_{4}^{5}$ に対する部分割り当ての行列表現

ここで幾つかの表記法を定義する. 部分割り当
同じ行にも同じ列にも 1 がないも$(u_{i_{1}})$$(u_{i_{2}})$$\mathrm{a}$て $A$ 中の $0$ で,

のを悪質な

$0$

と言い, それ以外の

$0$

を良質な

$0$

と

う. また, $\# BZ(\mathrm{A})$ で $A$ 中の悪質な の数を表す. 部分割り当て $A$ で, 変数がまだ割り当てられておらず (すなわち, $A$ の行列表現の $(i,j)$ 成
分が空白で) , $A$ の 列目にも 行目にも 1 が入っ言$\mathrm{s}$$0$$=\mathfrak{Q}$$x_{i,j}$$i$ていないとき例えば, 図$j$は生きている変数であると言う.
の部分割り当てをとした場合,$x_{i,j}$$1(\mathrm{b})$$A_{0}$

54$\# BZ(A\mathit{0}^{)}$

であり,

$0)$

2 (

$=$

$x_{2,4}$

はと $x_{2,2}$ に割り当てられた$x_{1,4}$

において生きている変数で$A_{0}$

ある.
$v$

を $B$ の頂点とし,た, 枝$(v, v_{0})$それぞれ $(x = 0)$ ,

き, 頂点

$v$

と

$v_{0}$

を$v_{1}$$v$の子とする. まと $(v, v_{1})$ に付けられているラベルを$(x = 1)$ とする.

このとで値の代入に選ばれた変数を $Var(v)$ で表す. すなわち $Var(v)=x$ である. 頂点 に対し, $Var(v)$ に が割り当てられた方の子 (上の例
) を $F(v),$ $Var(v)$ に 1 が割り当てられたでは方の子 (上の例では ) を $T(v)$ と書く.
$v$

$0$

$v_{0}$$v_{1}$

図 2: $B$ から作られた $S$ の–部分

ここでは, バックトラック木 $B$ の頂点数の下限を求めることが目的である. このために, $B$ からの作り方を説明する前に, ま
を作る.
別の木
$S$

$S$

の頂点集合はの持つ性質を示しておく.
$B$ の頂点集合の部分集合である.
従って の頂点数$B$のの頂点数の下限になる.
の下限はそのまま
葉以外の頂点はちょうど 1 つの子, またはちょうどn 個の子を持つ. また,の高さは である. より正確には, 根から各葉までのパスの長さはちょう
ず,

$S$

$S$

$S$

$S$

$S$

ど

$\frac{n}{2}$の根は $B$ の根は以下のように作る. まず,である.
の各頂点 に対して の子の集合 $CH(v)$を以下のように選ぶ. $CH(v)$ は最初空であり, 木$B$ をから下に辿ることにより, $CH(v)$ に頂点を1 つずつ加えていく. そのために, $B$ の頂点を $T(v)$ ,
$S$

$S$

$S$

$v$

$v$

$T(F(v)),$ $\tau(F(F(v)))(=T(F^{2}(v))),$... という順に辿っていく.
$(l\geq 0)$ が

$0$

を示す.

$i$

$0$

$(\tau^{\iota}(v))$

列目に 8 個のが悪質な である. )

$0$

は

列目に

$i$

$\frac{n}{2}$個の悪質ながあり, そのうち 5 個の

この場合,

$0$

$0$

$j$

As $(F^{l+1}(v))$

を含むことになり,

これ$\frac{n}{2}$

である.

$S$

の
行目には
を含んでおり, As
1 はないものとする. (図 3 に $n=12$ の場合の例

の悪質な

そして,

$\cdots,$$T(F^{\iota}(v))$,$Var(F^{l}(v))$

As $(F^{l}(v))$ に対して生きている変数であ以上 $B$ を辿って $CH(v)$ に頂点を加えることはしな

つまり,が最後に $CH(v)$ に選ばれた頂点となる. この場合, $|CH(v)| \leq\frac{n}{4}$ である. もし, $|CH(v)|< \frac{n}{4}$ であった場合は, 最後に選ばれい.

$T(F^{l}(V))$の子となる. 従って, この場合は はただ 1 つの子を持つ.
中の深さ の頂の作り方から分かるように,点に対応する割り当てには 1 がちょうど 個あるこた $T(F^{l}(v))$ が $S$ 中で

$v$

$v$

$S$

$S$

$i$

$i$

とに注意されたい. 以上の操作を, 根から全ての葉までの距離が$\frac{n}{2}$になるまで続ける.

るときに $T(F^{l}(v))$ を $CH(v)$ に加える. 図 2 は $S$ を作る際に $B$ をどのように辿るかの例を示したものである. 例えばこの例では, $Var(F^{2}(v))$ は $F^{2}(v)$の生きている変数ではないので $CH(v)$ に $T(F^{2}(v))$
は選ばれていない. このようにして頂点を選んでいき,$|CH(v)|$ が$\frac{n}{4}$になったところで子を選ぶのをやめる. この場合,$v$は$\frac{n}{4}$個の子を持つことにな

る.

しかし,

に達していない場合でも$CH(v)$ に頂点を加えるのをやめる条件がある. いずれかの列の悪質な の数が に達した場合には$|CH(v)|$ が$\frac{n}{4}$$0$$\frac{n}{2}$$CH(v)$ に頂点を加える操作をやめてしまう.

ことを正確に記述するために,

図 3: 頂点を $CH(v)$ に加えるのをやめる条件

このをまず, 任意のバックトラック木 $B$ から上記のよ考えてみる. As
であり, $Var(F^{\iota}(v))$ は x 吻であるとす高々4固る. また, As $(F^{l}(v))$ の 列目はちょうど

うに $S$ を構成可能であることを示す. これには,を構成するために $B$ の頂点を辿っている問に, $B$
がの葉に到達しないことを示せば良い. ここで,$(F^{\iota}(v))$

$B$

の頂点

の各列の悪質な$F^{l}(v)$
$0$

の数は

$\frac{n}{2}-1$$i$$\frac{n}{2}-1$

$S$

$u$

55

B の葉であるということは, As $(u)$ が $PHP_{n}^{n+1}$ をにするということであり, 従って, As $(u)$ には 1

$0$が 2 つある行が存在するか, 全て で埋まっている列が存在するかのどちらかである. 前者のような割り当ては, $B$ を辿る際にスキップしているので起$0$

こらない. 以下では後者の場合が起こり得ないことを示す.

の構成法により, ある列の悪質な の数がに達すると, $B$ のその先は見ない. 従って,
我々の見ている範囲では悪質な の数はどの列も高々である. $-$ 方,
時置深さ にある頂点$(v)$に対し As中の 1 の数は 個であり,は深さまでしかないので, 良質な (すなわち, 同じ行に1 を持った)の数はどの列においても高々 個である. よって, どの列もの数は高々 $n-1$ 個であり, 葉に到達することはあり得ない.
を $B$ 中の頂点とし, ある に対して
補題 2.
$v’=F^{l}(v)$ とする (図 4). $T(v’)$ が $CH(v)$ に加えられるなら, $\# BZ(A_{S}(F(v’)))=\# Bz(As(v’))+$
であり, $T(v’)$ が $CH(v)$ に加えられないなら,
$S$

$0$

$\frac{n}{2}$

$0$

$S$

$\frac{n}{2}-1$

$v$

$i$

$S$

$i$

$\frac{n}{2}$$0$$\frac{n}{2}$

$0$

$l$

$v$

考える. ただし, u。は根でありは葉である.
もし, $(u_{k-1}, u_{k})(1 \leq k\leq\frac{n}{2})$ が単純枝でないな
ら, $\# BZ(A_{S}(u_{k}))\leq\# BZ(As(u_{k-1}))+\frac{n}{4}-1$ で$u_{\frac{n}{2}}$

ある.

証明.

を考える.
をバックトラック木 $B$ 中の頂点で, $u_{k-1}$ に対応している頂点とする. すると, $B$ 中の $T(F^{l}(v))$ が中のに対応するような が存在する. 補題 2 より, $\# BZ(As(F^{l}(v)))-\# BZ(AS(v))$ は $T(v)$ ,$v$$u_{k}$$S$$l$$u_{k}$$T(F(v)),$ $\tau(p2(v)),$$\cdots,$$\tau(Fl-1(v))$ の中で $CH(v)$に加えられた頂点数に–致する. 以上の理由から,$\neq BZ(A_{S}(F^{l}(v)))-\# Bz(As(v))\leq\frac{n}{4}-1$

As

また,

$(T(F^{\iota}(v)))$

は As

となる.

のどこかのセル$(F^{\iota}(v))$に 1 を 1 個加えたものなので $\# BZ(As(\tau(F^{\iota}(v))))$となり, $\# BZ(A_{S}(\tau(F^{l}(v))))$$\# BZ(As(v))+\frac{n}{4}$ –1 である. すなわち,$\leq\# BZ(A_{S}(F^{\iota}(v)))$$\leq$$\# BZ(As(u_{k}))\leq\# BZ(A_{\mathit{8}}(u_{k-1}))+\frac{n}{4}-1k^{\gamma_{\mathrm{e}}}c$$\text{る}$.

$\square$

補題 4.

$1$

$\neq BZ(As(F(v’))).=\# BZ(As(v’))$ である.
証明. $T(v’)$ が $CH(v)$ に加えられるなら, $Var(v’)$

パス $P$ 中の頂点 $u_{k-1}$ と$S$中の任意のパス$P=u_{\mathit{0}}u_{1}u_{2}\cdots u_{\frac{n}{2}}$をは As $(v’)$ に対して生きている変数であるため, $F(v’)$

考える. ただし,は根でありは葉である.
もし, $(u_{k-1}, u_{k})(1 \leq k\leq\frac{n}{2})$ が単純枝であるな
ら, $\# BZ(.As(uk))\leq\# BZ(A_{S}(u_{k-1}))-\frac{n}{4}$ であ

では $Var(v’)$ の同じ行にも同じ列にも 1 がない.

る.

従って $Var(v’)$ に代入された
な
$1$

$0$

$u_{0}$$u_{\frac{n}{2}}$は As $(F(v)’)$ の悪質になり, $\# BZ(As(F(v’)))=\# Bz(AS(v^{;}))+$となる. 逆の場合, すなわち $T(v’)$ が $CH(v)$ に$0$

加えられない場合も同様にして示すことができる.
口

証明.

$B$

中の頂点

$v$

と $T(F^{l}(v))$ をそれぞれ,$S$に対応する頂点とする. 補題 3 と同様の議論により, $\# BZ(A_{S}(F^{l}(v)))-\# BZ(AS(v))$
であることが分かる. $Var(F^{l}(v))=x_{i,j}$とする. ( $u_{k-1}$ , u のが単純枝であるので, As
中の $u_{k-1}$ と$u_{k}$$\leq\frac{n}{4}-1$$(F^{\iota}(v))$

以上の議論により, 以下の特徴を持つ木 $S$ を作ることが可能であることが分かった.
の任意の葉から根までの距離はちょうど ある. また, $S$ の$S$$\frac{n}{2}$

の列

$i$

には

$\frac{n}{2}-1$

個の悪質な

$0$

がある.

ここで,

$x_{i,j}$に 1 を代入すると, 少なくとも個の悪質なを良質に変えてしまうため, $\# BZ(AS(\tau(F^{\iota}(v))))$$\leq\# BZ(A_{S}(F^{l}(v)))-(\frac{n}{2}-1)$ となる. よって,

$0$$\frac{n}{2}-1$

葉以外の頂点は子を 1 つ持つか,門持つかのいずれかである. ここで, 頂点 が子を 1 つだけ持つ
とき,とその子を結ぶ枝を単純枝と呼ぶことにす$\# BZ(A_{S}(\tau(F^{\iota}(v))))\leq\# BZ(As(v))-\frac{n}{4}$ ,わち,$\neq BZ(As(u_{k}))\leq\neq BZ(AS(u_{k-1}))-\frac{n}{4}$

る.

ある.

口

$\frac{n}{4}$

$v$

$v$

補題 5.

$S$

中の任意のパス

すな$P=u_{\mathit{0}}u_{1}u_{2}\cdots u_{\frac{n}{2}}$でを考える. ただし,は根でありは葉である.
$P$
このとき,中の単純枝の数は高々 である.
証明. $P$ 中の単純枝の数が n を超えると仮定す$u_{0}$$u_{\frac{n}{2}}$$\mathrm{B}\backslash _{\grave{\Lambda}}^{\backslash }10\backslash \mathrm{v}$.

$\frac{n}{4}$$-$.

$T(V’)\lambda^{V}10.pl\mathrm{v}’\mathit{1}$.
図 4: 補題 2 の例

る. パス $P$ に沿って悪質なの数を数える. 根では当然 $\neq BZ(As(uo))=0$ である. 根から下に行くに従って増加する悪質な$( \frac{n}{4}-1)(\frac{n}{4}-1)<.\frac{n^{2}}{.16}$

$0$

$0$

の数は, 補題 3 より高々である. また, 減少する悪質の数は, 補題 4 より少なくともである. よって, 葉では悪質な の数が負となり矛な$0$$\frac{n}{4}(\frac{n}{4}+1)>\frac{n^{2}}{16}$

$0$

補題 3.

$S$

中の任意のパス $P=u_{\mathit{0}}u_{12}u\cdots u_{2}$ を

56

盾である. 従って,
ある. 口

$P$

中の単純枝の数は高々レベルは $n^{C}n-i$ 個の項 $P_{[1,i+11},R^{(n}-i$ ) から成っていで$\frac{n}{4}$る. ただし,R(n-のは $[1, n]$ の部分集合でサイズは$n-i$ である. 第 $(n-1)$ レベルには$=n$ 個$n^{C_{1}}$$P[1,n],\{n\}$ が存在する.
}, $P[1,n],\{2\},$がただ 1 個存在す
最後に第 レベルでは空の項る. これまでに現れた項を, ここでは主項と呼ぶこの項$\cdots,$$P_{[1,\mathrm{n}],\{}1$$(\emptyset)$

$n$

個あるこ
とにする. 主項は全部でとに注意されたい. 図 6 は $n=4$ の場合の主項を表している. 列 , 行 に「 」 があることは, 項の$\Sigma_{i=0}^{i=n}(_{n^{C}i})=2^{n}$$i$

図 5: $S$ の単純枝の除去

中にリテラル $Xi,j$ が存在することを示している.

最後に, 図 5 のように単純枝を全て取り去って新しい木 $S’$ を作る. $S’$ の各頂点はちょうど 個の子醐嗣翻固\sim H 俳 コ] 唖醒繰羅睡郷$\frac{n}{4}$を持つ. また, 補題 5 より, 任意の葉から根までのパスの長さは少なくとも である. 従って $S’$ は,$+\mathbb{D}$$\frac{n}{4}$少な \langle とも$( \frac{n}{4})^{\frac{n}{4}}$個の頂点を持つ.

口

上述の証明において, 木 $S$ を構成する

注意.

際, 各頂点の子の個数, 各列に入り得る悪質な のに制限し,,数, 木 $S$ の高さをそれぞれ,$0$$\frac{n}{2}$$\frac{n}{4}$,

た. それらを,それぞれき,とすることにより,$\delta=\frac{1}{\log n}$$\delta^{2}n$$\delta n$

,

$+$

$i/$

$\frac{n}{2}$$(1 -\delta)n$と置$(\delta^{2}n)^{(-\delta)^{2}}1n\geq$$\ovalbox{\tt\small REJECT}++++$という下限を得ることができる.

$( \frac{n}{4\log^{2}n})^{n}$

図 6: 証明に現れる主項4

証明サイズの上限についてに対する –般の導出原理の証明サイズ
は $O(n^{3}2^{n})$ であることが知られている [4]. 本節で$PHP_{n}^{n+1}$

は, 文献 [4] の手法に工夫を加えることにより, 上限の改良を行なう. また, ここで得られた上限か

木状導出原理の証明サイズの上限も導く.

ら,

定理 2.

$PHP_{n}^{n+1}$

$Q$

$i$

$\in$

$Q$

かつ $j$$\in$$R$

である全てのリテラル$x_{i,j}$$i+$の和を表すこととする. また, $[i,j]$ で集合$\cdots,j-1,j\}$ を表すことにする.
(導出原理による)\ 証明の全体像をはじめに,示し, 後に細かな点について述べる. 証明の第 レ
ベルは 1 つの項 $P_{\{1\},[]}1,n$ から成る. 第 1 レベルはから成る. ただし, $R^{(n-1}$ ) は個の項$[1, n]$ の部分集合であり, そのサイズは $n-1$ である. よって, $R^{(n-1)}$ の取り方により $P_{[1,2],R)}(n-1$ は個の項個あるわけである. 第 2 レベルは$R^{(n-2)}$ は$[1, n]$ の
ただし,$P_{[1,3],R)}(n-2$ から成る.
部分集合で, サイズは $n-2$ である. 一般に第$\{i,$

$1,$

$0$

$n$

$n$

$i$

$i$

$PBP_{7}^{n+1}\tau$$i\text{レ_{}\mathrm{A})}\nu$$\{j1,j2,\cdots,j_{n-i}\}$$i$に対する導出原理の証明でサイズ $O(n^{2}2^{n})$ のものが存在する.
と $R$ をそれぞれ集合 $\{1, 2, \cdots, n+1\}$
証明.
と $\{1, 2, \cdots, n\}$ の部分集合とする. このとき, $P_{Q,R}$
は次に証明の細かな点について触れる. 第 レベルの各項は第 $(i-1)$ レベルにある項のうちの 個の項と中に元々存在する項から以下のようにを作の項 $P_{[1}1,i+$ ],作られる. 第るために, 第 $(i-1)$ レベルの 項 $P_{[1,i],\{j}1,j2,\cdots,jn-i,k$ }$(k \not\in \{j_{1},j2, \cdots,jn-i\})$
を使用する
まず,
を生成
各 に対して項}
第$(i1)$ レベルの項
このためには,する.

$P_{[1,2],R^{(}}n-1\rangle$${}_{n}C_{n-2}$

$i$

$k$

$\cup\overline{x_{i+1,k}}$$P_{[l,i],\{j}l,j_{\mathit{2}},\cdots,j_{n-}i$$P_{[1,i],\{j1,j_{2},\cdots,jn-}i,k\}$と $PHP_{n}^{n+1}$ 中の$i$$\overline{x_{i+1,k}})(\overline{x_{2,k}}+\overline{x_{i}+1,k})\cdots(\overline{x_{i,k}}+\overline{x_{i+1,k}})$良い. 次に, 今得られた 個の項$(\overline{x_{1,k}}+$,と $PHP_{n}^{n+1}$ 中の項 $P_{\{+}i1$ }, $[1,n]$ から,$i$$\overline{x_{i+1,k}}$個の項を使用すれば

$P_{[}$$j_{2},\cdots,j_{n-}i\}^{\cup}$

目的とを作る. 第レベルの項 $P_{[1,i1}+$ ],2 レベルの $P_{[1,3],\{1},4$ } を第 1 レベルの 2 つの項$P_{[1,2],\{4\}}1,3$’, から作る様子を図 7 に示にある
」 記号は, その項にリテ
す. 列 , 行
なる第$i$$\{j_{1,j_{2},\cdots,jn-i}\}$$P_{[1,2],\{\}}1,2_{l}4$
$i$

$j$

$\mathrm{r}-$ラル可が存在することを示している.
1 つの主項は $O(n^{2})$ ステップで個あるので, 証明サ生成される. 主項は全部で上記の証明で,$2^{n}$

イズは $O(n^{2}2^{n})$ である.

系1.

$PHP_{n}^{n+1}$

口に対渉る木状導出原理の証明で

57$FOCS’ \mathit{9}\theta$, pp. 274-282, 1996.

[2] M. L. Bonet, J. L. Esteban, N. Galesi and
J. Johannsen, “Exponential separations between restricted resolution and cutting planes
proof systems,” Proc.
, pp. 638-647,
1998.
$FOCS’ g\mathit{8}$$\mathrm{T}$[3] S. Buss, “Polynomial size proofs of the propositional pigeonhole principle,” Journal of Symbolic Logic, 52, pp. 916-927, 1987.

$\mathrm{f}$[4] S. Buss and T. Pitassi, ”Resolution and theweak pigeonhole principle,” Proc.
LNCS 1414, pp.149-156, 1997.

図 7: 主項の作り方,$CSL’ \mathit{9}7$[5] S. A. Cook and R. A. Reckhow, “The relative
efficiency of propositional proof systems,” .
Symbolic Logic, 44(1), pp. 36-50, 1979.
$J$

サイズ $O(n^{2}n!)$ のものが存在する.

証明.

定理 2 の証明中で作った導出原理による証

明を木状に展開する. 主項のみを考えると, 第 レ
ベルに 1 項, 第 $n-1$ レベルに 項, 第 $(n-2)$ レ
ベルに $n(n-1)$ 項存在することになる. 一般に, 第
$n$

$n$

レベルには $n(n-1)\cdots(i+1)$ 個の主項が存在する$i$

ことになる. 従って, 主項の数は $1+\Sigma_{i=0}^{i1}=n-n(n-$となる.

1 つの主項は $O(n^{2}.)$ ス
テップで作ることができるため, この証明木のサイ
ズは $O(n^{2}n!)$ である. 口$1)\cdots(i+1)\leq 2n!$[6] A. Haken, “The intractability of resolution,”
Theoretical Computer Science, 39, pp. 297308, 1985.
[7] P. Purdom, “A survey of average time analysis of satisfiability algorithms,” Journal of
Information Processing, 13(4), pp.449-455,
1990.

[8] A. A. Razborov, A. Wigderson and A. Yao,

5

おわりに

定理 1 および定理 2 から, $PHP_{n}^{n+1}$ に対する木状導出原理の証明サイズは, 一般の導出原理の証
明サイズの多項式では収まらないことが分かる.
今後の課題は, 文献 [2] の改良として, 木状導出原理と –般の導出原理の証明サイズがの比で異な$2^{\mathrm{c}n}$る例を見つけることである. 別の研究テーマとしては, $PHP_{n}^{n+1}$ に対する木状導出原理の証明サイズの上下限をさらに近付けることがあげられる. 本
稿で得られた上限 $O(n^{2}n!)$ と下限 (は, 共$\frac{n}{4\log^{2}n}\rangle^{n}$に$n^{(1-O}(1))n$と同じ比率で増加するという点において, ある程度厳密である. 今後の重要な研究課題はの下限を得ることである.

$\Omega(n|)$

参考文献[1] P. Beame and T. Pitassi, ”Simplified and improved resolution lower bounds,” Proc.

“Read-Once Branching programs, rectangular proofs of the pigeonhole principle and thetransversal calculus,” Proc.
, pp. 739748, 1997.
$STOC’ \mathit{9}7$[9] A. Urquhart, “The complexity of propositional proofs,” The Bulletin of Symbolic Logic,
Vol. 1, No. 4, pp. 425-467, 1995.