Derive Your Dreams

about me
Twitter: @kinaba

17:31 10/01/26

言語雑談会

言語雑談会 なるものに行ってきました。

自分は主に最近のD言語の話題 [PDF] [PPTX] についてと、 最近読んだ Pattern Calculus がイマイチ心に響かなかったという話と、 これも最近読んだ Prolog で SAT ソルバ という論文が格好良すぎて卒倒しそうです、などの話題を雑談していました。

SAT の話をしていてふと突然気づいたんですが、私が今までSATソルバに落としてみたことのある問題は、 すべて割と簡単に CNF(SATソルバがそのまま食べてくれる綺麗な形式の論理式) ができあがる問題だったようです、数独とか。 任意の命題論理式をCNFに変換できる指数爆発しない方法をそういえば知らないぞ俺!としゃべってたら soutaro さんが素晴らしい解説 をして下さいました。ありがたや。

あと shinhさんの 「コンピュータが遅い = メモリ足りない」から始まる発表がすごく面白かった。 いや、私は幸いなことに今のところマジメなプログラムでは真剣にメモリ不足に悩んだことはないんですけど、 Project Euler でいつも困るのがCPUパワーではなくメモリ不足だったので。 100倍遅いプログラムなら100倍時間をかけさえすれば動くけど、 100倍メモリを食うプログラムはそもそも動かないのだ。

光成さんの「RFCからずれてるメールアドレスを拾えるように、これとこれ "みたいなの" だけは許す、 と指定したら学習してくれるようなparserはないんですか」という話題も考えさせられました。 PRML Hackathon の時にやったような学習 の方向は、無から正規表現や文脈自由言語を学習する研究が主のような気がして、 そうじゃなくて、「基本はこれ」というベースの文法があって、 それを微妙に逸脱するものだけを系統的に救うようにその差分だけ自動で学習…という方向は楽しそうです。

22:32 10/01/14

最短性をチェックする

迷路の最短経路を求めよ』 という問題が、自分の周辺で物議を醸しているようなのです [1] [2] [3] [4] ─ 求めるのはいいんだけど、Lv2 ~ Lv4の「最短性のチェック」って何をしろというのですか、 わかりません!

出題された方の意図を勝手に察すると、 「必ず最短の経路を求めるアルゴリズムが作れた」 あるいは 「必ず最短を求めるアルゴリズムである理由が説明できた」 くらいの意味なのでしょう…… というのは皆様もちろん承知の上で、でも、そう解釈するよりも文字通り解釈した方が遙かに面白い問題になりそうなのではしゃいでらっしゃると思うのですが、私も悪ノリしたくなりました。

問題: 返す解が本当に最短であることのチェックまでしてくれる迷路ソルバを作ろう。

(※ カンペキに格好いいアプローチとしては、 Coq や Agda 等、今流行の「証明が書けるプログラミング言語」を使って迷路ソルバを実装すると同時に、 そのソルバが必ず最短路を返すことの証明まで実装してやるという手があります。 機械検証された最短性証明つきソルバを作れば、これはもう文句なく最短性のチェックまで正しくできた、 と宣言してよいでしょう。きっと誰かやってくれると思うので、 私は他のアプローチをとってみます。) (※追記: yoshihiro503 さんがやってくれました!

深く考えずチェックする

要はこういう関数が書ければ、チェックできてると言っていいですよね。

def is_shortest(answer)
  # ソルバの出力 answer を受け取って、最短ならtrueを返し、でなければfalse
end

answer = can_be_incorrect_solver( gets(nil) )
if !is_shortest(answer)
  puts "最短じゃない!"
end

どう書けばいいか…全部の可能なルートを列挙してみて、そのどれよりも短ければOKだろう!

def is_shortest(answer)
  for r in all_possible_routes()
    return false if length(r) < length(answer)
  end
  return true
end

…これは、問題のページにも書かれているとおり可能な経路の数が多すぎるので、 現実的な時間では終わりません。無理です。他の手段が必要です。どうしましょう。

ええと、実際に最短経路の長さを計算してみて、それと同じ長さになってたら最短経路と言えるんじゃない!?

def is_shortest(answer)
  input = answer.gsub("$"," ")
  return length(compute_shortest_route(input)) == length(answer)
end

ちょっと待てい、と誰もが思ったと思います。はい、駄目です。 最短経路のルーチンが正しいかどうかチェックしたい時に、 その中でまた最短経路を計算してたら、いったい何をやっているのかわかりません。 compute_shortest_route が本当に最短経路を返すことが確実でないと、 これではなんのチェックにもなりません。堂々巡りです。

(※注: 問題によっては、この実装が正解であるケースもあります。 ひとつは、たとえば最短経路を求めるよりも、 最短経路の長さだけを求める方が遙かに簡単、だった場合。 length(compute_shortest_route(...)) を、 経路ではなくその長さだけを求める遙かに簡単な関数として実装すれば、堂々巡りにならずに済みます。 ただし今回の場合、「長さだけを求める」のも難易度が変わらないのでダメっぽいです。 もうひとつのケースは、既に正しいと確信できる既存の実装があって、それを参照実装として使える場合。 例えば、正しく動くんだけどソースが汚くなってきたので置き換えたい旧バージョンの実装と新バージョンを比べる、 とか、すごく遅いので小さいデータにしか使えないけど、シンプルで明らかに正しいと確信できるような実装と、 小さいデータでだけ比較する、とか。)

さて困った。

本気でチェックする

もっと深く「最短路」のもつ性質を考えなければならない時が来たようです。

*************
*S  $$$$    *
*$$$$  $$$$G*
*************

たとえばこれが最短路でないのは、何故か?それは…

*************
*S  $$$$    *
*$$$$  $$$$G*
*************

この無駄な経路の代わりに

*************
*S          *
*$$$$$$$$$$G*
*************

こう近道ができるからです。要は、

*************
*S  $$$$    *
*$$$X  Y$$$G*
*************

この X と Y の間に、今の $ 4個とは別の、もっと短い道があるからこそ、最短路ではないと言える。 さらに徹底的に言い直すと

*************
**  ****    *
****S  G*****
*************

この迷路の S と G の間に $ 4個より短い最短路があるから、元の経路は最短路ではなかったのです。 逆に、経路上のどの X, Y をとってもこういうショートカットが存在しないなら、それは確かに最短路と言えます。 というわけで、この条件を素直に実装します。

def is_shortest(answer)
  for X in all_points_on_route(answer)
    for Y in all_points_on_route(answer).select{|y|y!=X}
      newmaze = answer.gsub(/[S$G]/, "*")
      newmaze[X]="S"; newmaze[Y]="G"
      return false if length(compute_shortest_route(newmaze)) < current_length(X, Y, answer)
    end
  end
  return true
end

また compute_shortest_route が出てきていますね。 これも残念ながら堂々巡りなのでしょうか…。

いいや、そんなことはありません! …というのが、この記事の本題です。前振り長かった…。 この、今実装途中の 完成してなさそうな is_shortest と、今まさに正しいかどうかチェックしようとしてる途中の 合ってるか間違ってるかわからん最短路ソルバ があれば、正しさをチェックするには十分です。こうする。

      ...
      newanswer = can_be_incorrect_solver(newmaze)
      return false if !is_shortest(newanswer)
      return false if length(newanswer) < current_length(X, Y, answer)
      ...

can_be_incorrect_solver の返す結果は本当の最短路ではないかもしれないので、 本当にこれが最短路になっているのか、念のため、is_shortest を再帰呼び出ししてチェックします。 もしチェックが通らなかったら…今検査中の answer が最短路かどうかはもうどうでもいい。 そんなことより、最短路ではない newanswernewmaze の最短路として返してしまっている! これはもう、どっかにバグがあること確定です。return false です。 もしチェックが通ったら、これは確かに最短路なので、安心して、予定していたとおりに、 元のX-Y間の$の数と大小比較に使います。

(※注:「これは確かに最短路なので」って本当でしょうか? is_shortest の中で再帰して is_shortest を呼んだりしてるけど、どうやってそんなのが正しいと言えるのか…というと、 これは、newmaze を作るたびに壁 "*" を増やして再帰呼び出ししているので、 だんだん動ける場所が少なくなっていくことを利用して数学的帰納法で証明できます。できると思います。はい。)

というわけで、できました。間違ってるかもしれないソルバ を使ってそれ自身の正しさをチェックするチェッカーの完成です。

...from their errors and mistakes, the wise and good learn wisdom for the future. - Plutarch

具体的な実装

具体的な実装に進む前に…ここまでの話の中で、2つほどゴマカシがあります。 一つは、is_shortest って名前、おかしいですよね。 パラメタ answer が最短路じゃない場合に false を返すのはいいんですけど、 最短路だったとしても、チェックの途中で newanswer が間違ってると false を返してしまうのは…。 例えルーチンがバグってようとも「answer が shortest じゃない」みたいな答えを返すのは、名前がヘン。

というわけで、インターフェイスを変えて、checked という名前にします。

# チェック対象の迷路ソルバルーチン
# shinhさんのゴルフ実装をお借りします
def shinh_solver(maze)
  q=($_=maze*1)*1,~/S/
  (a,i,*q=q
  a[i]<?S&&a[i]=?$
  4.times{|x|q+=[a*1,x]if$_[x=-~x%3*-~~/$/-~/$/+-x/2+i]!=$_[x]=?*})while/G/
  a
end

# こうやって呼び出すと、結果が最短路じゃなかったら例外を飛ばす
# このルーチンは正しいはずなので、例外は飛ばないはず
checked(method(:shinh_solver), "*********\n*S   * .....")

# わざと間違えてDFSにしてみた
def shinh_solver_dfs(maze)
  q=[[($_=maze*1)*1,~/S/]]
  (raise "hoge" if q.size==0
  a,i=q.pop
  a[i]<?S&&a[i]=?$
  4.times{|x|q+=[a*1,x]if$_[x=-~x%3*-~~/$/-~/$/+-x/2+i]!=$_[x]=?*})while/G/
  a
end

# これは例外が飛ぶ
checked(method(:shinh_solver_dfs), "*********\n*S   * .....")

こんな感じに使う。

もう一つのゴマカシは非常に酷くて、 実は、このチェック方法は、対象のソルバが元記事でいう 「Lv2:最短性のチェックはせず、とにかく1本の到達経路を求めることまではできた」 まではクリアできていることを前提条件としてしまっています。 間違ってるかもしれないけどそんなに酷く間違ってはいないソルバ を使ってそれ自身の正しさをチェックするチェッカーと言わなければいけませんでした。 この前提をどうやったら外せるか、上手い案が思いつかないのですよね…。 どこでこの仮定が必要になるかは、以下の実際のソースをご覧下さい。

class NotShortest   < StandardError; end
class RouteNotFound < StandardError; end

def checked(solver, maze, want_length=false)
  # まずは solver で迷路を解いてみる
  answer = solver[maze] rescue (raise RouteNotFound)

  # 返ってきた答えから $ の道を取り出す
  r = extract_route(answer) or (raise NotShortest)

  if r.size > manhattan(maze, r[0], r[-1]) # 高速化用: マンハッタン距離と一致すれば明らかに最短
    for i in 0 ... r.size
      for j in i+2 ... r.size
        begin # r[i]とr[j]を繋ぐ、今(j-i+1)より短い近道があったら死亡
          raise NotShortest if
            (j-i+1) > checked(solver, wall(answer,r[i],r[j]), true)
        rescue RouteNotFound # ← ココ!RouteNotFoundが返ってきたら、
        end                  #    本当に道がない==近道もない、と信じて無条件でチェックを通す
      end
    end
  end

  # 近道がないなら確かに最短。答えを返す
  return (want_length ? r.size : answer)
end


def wall(maze, s, g)
  # s, g を残して、元々あったルートを壁 "*" にする
  maze.gsub(/[S$G]/, "*").tap{|m| m[s],m[g] = "S","G"}
end


def extract_route(maze)
  w = maze.index("\n")+1 # 横幅

  p = maze.index("S") or (return nil) # 開始点
  route = [p]
  until maze[p] == ?G
    nexts = [p-1, p+1, p-w, p+w].select{ |t|             # 上下左右
      !route.include?(t) && (maze[t]==?$ || maze[t]==?G) # のうち次のマス
    }
    return nil if nexts.size != 1 # 分岐 or 行き止まり。おかしい
    route << (p = nexts[0])
  end
  return route
end


def manhattan(maze, s, g)
  w = maze.index("\n")+1
  (s/w - g/w).abs + (s%w - g%w).abs + 1
end

まとめ?

あ、3つめのゴマカシがありました。 実は、最悪の場合の計算量は、全部の経路を生成するのと同等かそれ以上に悪いです。 けど、まあ、マンハッタン枝刈りのおかげで、時間がかかるケースを作るのは結構難しいのじゃないかと思う。 ので、それなりには使えなくもないかもしれない。知りません。どうだろう。

あと、「このチェックが正しいという保証はどうするの?」というのはFAQだと思いますが、 最短性のチェックを書いただけで最短性のチェックのチェックは書いてないので、そんな保証はないです、 という答えになります。というかこれ、本当に正しいんでしょうか。いまいち自信が…

presented by k.inaba (kiki .a.t. kmonos.net) under CC0