終盤DBの可能性?(3)
日がな考えて何がまずいかやっとわかったorz
ちょー単純な話だった。n_
定理1と称していたものは、判定しようとする局面sがn手詰であることを最初に仮定したとき何が起きるかを述べているだけで、sが本当にn手詰局面かどうかについて十分には言及しない
すわなち、
命題A: 目下の局面sが玉方をn手先までに詰ませられる*1局面である
命題B: 目下の局面sから先に、sのn手先までに決して詰ませない玉方の応手が存在する
として、確かにn手詰の定義からB→¬A = ¬A∨¬Bは真だと言えるから、sがA∧Bを満足することは有り得ない、すわなち、sが互いに背反な条件¬A∧¬B、A∧¬B、¬A∧Bのどれかを満足することまでは言える。しかし、これらの論理和が元の¬A∨¬Bに他ならない以上、¬A∨¬B自体はsがこれらのうちのどれを満足するかを導かない。
よって、この判定は、探索等の別途手段で解決せねばならない。
それはそうとして、無理矢理¬Bと仮定して探索すると何が起きるだろうか？
運良くsが¬A∧¬BかA∧¬Bを満たす局面であれば、¬Bを仮定しても正しく判定でくる。
不運にもsが¬A∧Bを満足する局面であったなら、不詰みを詰みと判定する危険のみ生じる（←重要）
ただし、どっちが生じたのかは、¬Bの仮定を外して厳密に探索しないとわからない。
従って、¬Bと仮定して探索し、不詰みという結果を得たなら、それはsが明らかにn手詰局面でないということで、スクリーニングに使えることが考えられる。*2
一方、詰みという結果が出たなら、sが本当は¬A∧Bであるところを不完全な探索で誤った（実際は詰ませるためにn手より大〜∞の手数を要する）か、あるいは本当にn手詰局面であるかのいずれかである。これは完全な探索で改めて調べる必要があるが、それでも計算の省力化の余地があり、孫ノードにn-2手詰でない局面が出現する等すれば、ただちに不詰みとわかる*3
よって定理1は便利なのだ、1手詰、3手詰、5手詰と順番に調べていくことは効率がいいのだ、と強弁して終わる*4
なお、本方式は不詰み判定におけるNB0AMG法と呼ぶ
