|
・あくまで継電連動装置に即して読み解く「連動（interlocking）」
・Google Scholarが「肩すかし」だと感じたら：「関連キーワード」の選びかた
（約17000字）
「研究ホワイトボックス」としては、「混雑率」（[3051],[3052]）、「空気系統」（[3137]）に続き、鉄道に関する研究の話題です。
とはいえ、「研究ホワイトボックス」は「話題」を提供することが目的の記事です。例えば、▼鉄道の研究はしていないがアルゴリズムの研究をされているかた（学生を含む）が、何を学べば鉄道のアルゴリズムの研究もできるようになるのだろうか、あるいは、▼鉄道の研究をしているにもかかわらず最新のアルゴリズムの研究動向には明るくないというかたなどおられたときに、仮には『若手！』（[3179]）が何をジョウシン…いえいえいえ、いかなるレポートやレビューを「上げ」（※）ればいいんでしょうか、といったことを、紙上（≒ウェブ上）で仮想的に体験いただければなぁ、という「ねらい（めあて）」でございます。
※結局、「上げ」るんですね、わかります！
・[3179]
> 1959年、社長に就任した＊D＊はコンピュータに対する関心が高く、＊A＊を始めとした若手エンジニアが専門知識の講義を行った。
> こういうソレであれば「えきすぱぁとしすてむっ！」（[3166]）にはならないんではないかなぁ、と、改めて思われました。
※臆することなく「講義」できるためにも、早くは「校長先生と給食！」（[3096]）が『指数的に効いてくる！』（[3152]）と…思いますよねぇ。
この記事では、鉄道の「連動装置」（interlocking）に関する研究が、単に装置の開発（「ものづくり」としての高信頼化など）という話に留まらず、数理的な問題（ソフトウェア、アルゴリズム）にもわたっていることを認識します。そして、現在、どのような研究が進められているのかを概観します。
…という一種「内容面」の流れとは別に、全体として▼情報の探しかたや選びかた（英語で）、▼勉強のための遊びかた（プログラムをもらってきて動かしてナットクしよう、の意）、というはなしになっていますから、内容は別として、そのような一種「機能面」だけをご活用いただければとも思います。
●あくまで継電連動装置に即して読み解く「連動（interlocking）」
「連動装置」を読み解く、その一歩手前っぽい話です。
・[3233]
> 「連動装置」を、NHKや全国紙のレヴェルの語彙で説明せよ、と（ふつう、いわれませんけれども）いわれたとしますと「ポイントと信号機を適切なパターンで安全に操作する装置」と書きかけ、しかし、D-ATCやATS-Pの「パターン」の説明とまぎらわしいぞ、といって、ええい、「真理値表」を持ち出したほうがよほどすとーんとすとすとまいるではないか、といってみたくなりました。うまい紹介のしかたを考案できましたら、しめしめといって、その実、このサイトの連動装置の項の記述が一新されるということです。…そんなにうまくいくものですか。
※すとーんとすとすとまいる：腑に落ちる、しめしめ：あわよくば。
その点は後回しにしまして、ここでは先に文献を探し、見つかった文献に即しての理解を目指すという流れでまいりましょう。結果的に、継電連動装置（≒実装にリレーが用いられた時代の連動装置、の意＝『カチカチ』[2856],[3170]）に即しての理解ということになりましょう。それでいいのか、もっとわかりやすい理解のしかたがないのかは、別途、考えることにいたしましょう。
・「連動装置の制御論理を可視化する」鉄道総合技術研究所RRR（2011年）
http://bunken.rtri.or.jp/PDF/cdroms1/0004/2011/0004005434.pdf
> 駅毎の制御条件を記述した“連動図表”
> 継電連動装置と結線入力式の電子連動装置では，制御論理を記述した“連動結線図”
『「新形でない」電子連動装置』がいかなるものであるのかわからずにいたのですが、なるほど、継電連動装置を扱ってきた技術者が従来通り作業できるよう、インターフェースを「結線入力式」としてある（初期の？）電子連動装置があるんですね。
インターフェースだけを見れば確かにレガシーともいえます（[2729]も参照）が、これがどうして、しかるべき後にインターフェースの「ボード1枚」（あくまで例えです）差し替えるだけで「新形」と同様のシステマティックな（デジタルな）制御（＝上位システムとの接続）に対応できるのであれば、何も問題はありません。本当でしょうか。
※さらには、継電連動装置であってもインターフェースを取り替えたり『読み替え』たりしながら『（わが社の）うんこうかんりしすてむっ！』（[3270]）と呼んでいこうというのも合理的な取り組みかたの1つであることは疑われません。しかし、（時代や設計思想の異なるものが近接して混在するという意味で）あまりにも雑多になったり、著しく古い箇所など残っていたりするのは問題のもとになるのであろうと、これまた籠原駅のほう（[3191]）など遠巻きに眺めながら思ってみようかと思いました。（恐縮です。）
> 設計のコンピュータ化にあたっては，多くの作業を自動化できますが，作成過程において設計者の判断が不可欠であり，設計図面を全体的に見渡すことも必要です。このため，従来から行われてきた連動図表と連動結線図の作成を踏襲し，設計者を支援するという立場からシステム開発を行い，作成過程における自動化と様々な情報自動表示を実現しました。
これまでの手法をなるべく「踏襲」すべし、という一種「お達し」に抗えないお立場であれば（これはひどい無理難題だ、といって）お気の毒さまですが、そうではなく、特段の検討もされないまま「踏襲するのが当然である」というところからスタートされている（一種「頭が凝り固まっている！」）のであれば、なかなか（研究を展開していくのが）苦しいのではないかと見受けられます。
・[2729]
> ATACSは本来、軌道回路に頼らない列車運行を目指して開発されています。駅間の閉塞信号機は不要になり、閉塞信号機を動かすために必要な駅間の軌道回路も不要になるでしょう。しかし、連動駅構内の軌道回路をなくしてしまうには、連動装置を含めた変革が必要になります。
※「ATSからATACSへ移行したときの利点」（「C-ATS」[3117]も参照）と「ATCからATACSへ移行したときの利点」（「無線式ATC」同じく[3117]）を区別できていない「素朴な疑問」であったとわかります。
このあたりの「素朴な疑問」をまとめて解消できそうな発表が、約6年後の2012年3月になされていました。いまわからないことは、とりあえず待ってみるものだ（「公知」になってから知る立場としては、常に遅れて知ることになります、の意）と実感されます。
・「第２５４回 鉄道総研月例発表会」（2012年3月14日）
http://www.rtri.or.jp/events/getsurei/2012/Getsu254.html
「無線」で「地上連動装置と軌道回路を省略」といったテーマに取り組まれつつも、「耐ノイズ性の高い」軌道回路や「連動結線図自動作成システム」にも取り組まれるという、いま絶妙に在来線（や鉄道総研）の置かれた立場がうかがえる発表会になっているやのように見受けられます。（あくまで感想は個人です。）
※もちろん、これらのテーマは互いに対立するとは限らず、都心部の線区では無線制御になりつつも連動装置を排するまでは至らない（当面、至らない）んだとか、「バックアップ」（[3105]）として従来の信号や軌道回路も残されるんだといった見通しがあるのかもしれませんし、そうではなく単に、いろいろなスパンのテーマが入り乱れているんだとも見えます。部外者にはわかりかねます。
・「連動図表と連携した連動結線図自動作成システムの開発」鉄道総研月例発表会講演要旨（2012年3月14日）
http://bunken.rtri.or.jp/PDF/cdroms1/0011/2012/0011002085.pdf
> （前略）
> 結線図をコンピュータによって自動生成するためには，その概念を構造化することが重要である。構造化方法として，連動図表作成支援システムと同様にオブジェクト指向により行った。
> （全略）
> ●で表されているのが集約結節点であり，
※「●」は緑色。えっ！！ 本文中で緑色の「●」ですと。…うーん。
必要とされつつ、重要な仕事だとは思われつつも、しかし、いまモーレツに「車輪の再発明」感が高い（[3052]）と感じられるのは気のせいだといっては「過言」だと思います。よくない意味での「便利な定規」（[3089]）をつくろうというのは『非常にわかりやすい』（※）ことであり、いま素朴に一種『ポイントが高い』テーマではありましょうが、その分、類似のものや簡易に活用できるものが既に存在していないかしっかり調べる＝調べ尽くすということが要求されてきます（調べが甘いまま取り組んでいると後からクロウしそうです、の意）。
※一種「査定」する「上」にもわかりやすく、一種「実働部隊」たる「下」にもわかりやすいので「士気のようなもの」がたやすく高まり、専門でない「外」の人に対しても成果がわかりやすい（ので一種「有利」である）、の意。
※「便利すぎる定規」とでもいいましょうか、あまりにも便利ですと、使う人が何も考えなくなるおそれが高まってまいりましょう。「モラルハザード」（ただし大辞林による）の一変種とみてもよいのではないでしょうか＆もっと本当でしょうか。ハハハ！ この『定規』を使っている限りゼッタイ、ダイジョーブっ！ …的なソレということです。『定規』があってもなくても払わなければならない注意を払わなくなる、の意。
・Weblio じしょびゅう 「三省堂 大辞林のモラルハザード（1）と（2）の中間くらいの語義を想定しています（仮）」付近
http://www.weblio.jp/content/%E3%83%A2%E3%83%A9%E3%83%AB%E3%83%8F%E3%82%B6%E3%83%BC%E3%83%89
※「（1）保険」に限らないという意味で「（1）」を超え、しかし「（2）節度のない利益追求」とまではいわない、「（1.5）くらい」の語義がほしいですよねぇ。
▼作成された連動結線図（図といいますか、結線＝回路そのもの）のテスト（検証）を自動化できるよう目指さずしてどうするのか（テストにおける人のミスをどう訂正するのか＝そこもあくまで人なのか）、▼その手の自動化のツール（回路設計や基板レイアウトの類）は既にいろいろあるのではないか＝既存のツールに合うように連動図表を表現する記法を検討するのが当座のテーマになるのではないか、▼それすらも国内外の信号メーカーが既に行なっているのではないか、▼（あくまで自前で検討・構築するとしても）ネットワーク構造（一種のフローチャート）の編集や可視化だけ既存のツールを使う方法もあるのではないか（Excelと工程表[3096]も参照）、などと疑われます（＝2011年、2012年のいずれのPDFとも、参考文献が挙げられていないため、形式上、いっさいサーベイされていないとみなされます[3093]、の意）。
●Google Scholarが「肩すかし」だと感じたら：「関連キーワード」の選びかた
とりあえずGoogle Scholarで探しますと、いろいろ出てきます。
…と、ひとことで済ますのではなく、実際にリンクいたしましょう。
・Google Scholar 「railway interlocking」の検索結果です（検索語はイメージです）
https://scholar.google.co.jp/scholar?q=railway+interlocking&btnG=&lr=
いわゆる「検索窓」に何を入れたらいいのか、というのが、最初にして最大の「難かん」であるのです。たぶん。
・[3102]
> しかし検索窓で「昭和時代」といっても
・[3059]
> 検索窓に何を入れたらいいのか
・[3287]
> ＊＊＊の何かをあらかじめ制約するようなことに対しては、＊＊全体でシビアに問うていこうではありませんか。
> 英語のデータシートも読む（データシートの所在を英語で探すところから含む）のは、もちろんです。
※言語を問わず、情報の探しかたについては[3182]も参照。フレッシュな時期（みんなできなくてあたりまえ、できないことを責められたりしない時期、の意）に、ぜひ「図書館ツアー」をば！ 学生のうちに未履修…いえ、未参加であられますならば、職場の図書館（や図書室）の同種のソレを逃さず参加なさってください。2回も3回も参加するものではないですが、0回（未参加）というのは、たいへんよろしからぬ状態であると自覚いただけたらなぁ、などと、そこまでおっしゃることは通常ない「図書館のほうのかた」のほうなど思い浮かべながら勝手に申してみます。（恐縮です。）
・（参考）「職場の図書館」のイメージです
http://www.rtri.or.jp/link/rail_museum_J.html
http://www.jsla.or.jp/about_jsla/member_organization/kanto_kaiin/
https://calil.jp/library/special
これに対し、Googleと呼ばれる「巨じん！」は肩の上から肩すかし…いえ、「関連キーワード」を投げかけてくれます。…いたたた（※）。
・同
> 関連キーワード
> railway interlocking systems
> railway interlocking safety
> railway interlocking signalling principles
> railway interlocking plc
> railway interlocking modelling
> railway interlocking petri
> railway interlocking specification
> railway interlocking safety-critical systems
> railway interlocking trains
> railway interlocking uml
> railway interlocking component-based
> railway interlocking safety requirements
> railway interlocking signal
> railway interlocking model checking
> railway interlocking safety verification
おおー。それらしいのが並びました、と見るか、これはなんだ？ と思うかは分かれましょう。しかし、無意味なものや無関係なものは出てくるはずがないと一種「盲しん」して、知らない語があれば、すべてきちんと調べ尽くしましょう。それがサーベイというものです（[3137],[3169]）。
※「関連キーワード」が示されるのは、あなた、なに探してるのかわかんなーい、とGoogle先生に一種「投げられた」という状況であるのです。…いたたた。
ここでは、仮に「formal method」という、「関連キーワード」にも出てこなかったソレが…気になります！ …といって、近づいてじっと見てみましょう。
・「THE ROLE OF FORMAL METHODS IN DEVELOPING A DISTRIBUITED RAILWAY INTERLOCKING SYSTEM」（2005年7月14日）
http://fmt.isti.cnr.it/webpaper/forms_04.pdf
内容のよしあしや検索の目的との適合とは別口で、著者やその所属やいかにといって、特に外国のことはよくわからない、他分野のことはよくわからない、といって、地味に困ります。そこを調べるのもサーベイのうちですね。
・「Istituto di Scienza e Tecnologie dell'Informazione」（in English）
https://en.wikipedia.org/wiki/Istituto_di_Scienza_e_Tecnologie_dell'Informazione
・「CNR Research Area of Pisa」（in English）
http://www.area.pi.cnr.it/index.php?lang=en
いかなる研究組織であるかの理解が追いつきませんが、（イタリアにおける、国の）研究評議会（日本にも独立の組織や委員会はいろいろありますが、研究に関して実際的な権限を持つ委員会等は設けられていません）に属する研究所で、貢献の大きかった人の名前を冠している（「大隈講堂」「福武ホール」的なソレの、建設資金などでなくあくまで研究上の貢献に基づくもので、建物でなく研究所組織そのものに冠せられる、の意）、日本にはない形態の、しかし（日本国内でいえば「国の」と形容しうる：大学共同利用機関法人がもっと独立して、自前で大学院大学を持ったような、というのともちょっと違うような）日本でいえば筑波や京阪奈のような「学研都市」である「CNR Research Area of Pisa」に立地しているとのことです。仮には「産総研みたいなの」と曲解しておけば当たらずとも遠くないのではないかと想像してみます。（あくまで想像です。）
2011年には、SPIREと略される情報系の（比較的）小規模な国際会議をホストしているようで、しかし、行ってみたら筑波や京阪奈のようで変わり映えせず、というガッカリ感（時計台にも劣らないソレ）があったかもしれません。
・Google ストリートビュー 「CNR Research Area of Pisa」付近
https://goo.gl/maps/exizLMZVcvJ2
https://goo.gl/maps/BcjFZeMth2C2
https://goo.gl/maps/S4YxSxTy1tx
https://goo.gl/maps/hb9RfdECsbJ2
https://goo.gl/maps/E3M7nciG2yS2
※どう見ても筑波や京阪奈です＊＊＊＊＊＊＊＊＊＊たー的なソレだと思えてきそうです。
・「SPIRE 2011」
http://spire2011.isti.cnr.it/
http://spire2011.isti.cnr.it/?page_id=252
※5日間のうち、初日はチュートリアル、最終日はワークショップで、メインのセッションは3日間に10つ、計39件の発表があったということです。セッションはパラレルではなく、きわめて濃密に「かわいがられる」系のソレとお見受けしました。しかも、3日かけて参加者の頭の中がほとんど同じになった状態で、「『みんなの』今後の課題」としてのワークショップに取り組むということで、なかなかさようさようごもっともごもっとも、最終日にいかほどの「やわらかあたま（驚きの真っ白）」が発揮できるかといえば難しそうで、むしろ、教育的な側面のほうが大きいのかなぁ、などと邪推します。（あくまで邪推です。）
・「SPIRE2011の論文でweb公開されているものをリストアップしてみた」（2011年10月30日）
http://d.hatena.ne.jp/echizen_tm/20111030/1319976044
> SPIREで発表された論文については例年Springerからまとめた書籍が発売される。が、無料で済ませられるならそれに越したことはない。というわけでSPIRE2011の論文でweb公開されているものをリストアップしてみた。
※いや、まぁ、その、学生としては「研究室で1冊買ってくださいお願いします」するのが先ですから、学生のかたにあってはどうか、センセイとのコミュニケーションを疎まず惜しまずお願いしたくあります、たぶん。
※2012年はコロンビア、2013年はイスラエル、2014年はブラジル、そして2015年はロンドンとのこと。他の会議等も含め、気になった論文については「続報」（『後輩』の学生に引き継がれたものを含む）もお読みになるようご習慣ください、ぜひ。Springerで出版されてもなお、あくまで「速報値」です。特に、「ハイパーパラメータの推奨値」などを予稿から拝借して実装されるにあっては、続報や他者の論文で「やっぱり違った」と否定されていないか、一種「無効資料調査（公知資料調査）」のようなクロウが求められてしまいます。それを自分ではハンドリングしかねるといって一種「投げる」場合は、しかるべき「教科書」が出るのを待ちましょうということです。
・「SPIRE 2015」
http://www.dcs.kcl.ac.uk/events/spire2015/
・任天堂「やわらかあたま塾」（2005年6月30日）
http://www.nintendo.co.jp/ds/ayaj/
・任天堂「Wiiでやわらかあたま塾」（2007年4月26日）
http://www.nintendo.co.jp/wii/rywj/
内容としては「形式手法（Formal Method：「FM」とも）」を応用しましょうということのようです。
・ウィキペディア「形式手法」
https://ja.wikipedia.org/wiki/%E5%BD%A2%E5%BC%8F%E6%89%8B%E6%B3%95
https://en.wikipedia.org/wiki/Formal_methods
> この記述は GNU Free Documentation License のもとに公開されているコンピュータ用語辞典『Free On-line Dictionary of Computing (FOLDOC)』に基づいています。
とのことで、日本語版だけおかしなことが書いてあるということはないようです。
さて、「railway interlocking」などという検索語を投げて肩すかしが返ってくるような初学者としましては、あまり具体的すぎず、個別の応用に進みすぎず、源流といいましょうか、「基礎からバッチリ」なエリン（[3103]）を目指してみたくなってきます。
そこで「railway interlocking modelling」で検索しなおします。
・修士論文「Modelling Interlocking Systems for Railway Stations」デンマーク工科大学（2008年）
http://etd.dtu.dk/thesis/221879/ep08_68_net.pdf
「鉄道の連動装置をモデル化し、（既成の）モデル検証ツールにかけ、その結果を表示するシステム（Javaベース！）や、そのための記法（XMLベース！）をつくりました！」という、いかにも修士論文らしい修士論文（≒パワフルでたくましい、の意）のようです。…といって、「メタ目次」（[3093]）でいう「5章」にあたる箇所のみを読んでみます。
> 12.1 Project summary
> The goal of this thesis was to develop a formal method for verifying that inter-locking systems for railway stations guarantee the safety of trains.
> In order to do so, we have studied and modelled relay interlocking systems for Danish railway stations: static and dynamic models have been specified on different levels of abstraction. Furthermore, a transformation from an instance of a static model to an instance of a dynamic model and its associated confidence conditions has been specified using RSL and afterwards implemented using Java.
> （略）We have formulated patterns for the behaviour of external inputs to interlocking systems. The dynamic model must be extended with instances of these patterns such that it includes the interaction with the external world. Also, patterns for safety properties have been developed.
> （略）Altogether, the work presented in this thesis has successfully defined a method that uses ordinary station documentation as a starting point for verifying that interlocking systems guarantee the safety of trains at a station. It has been demonstrated that the method is fully applicable to a small Danish railway station. However, as the method has not been applied to larger stations, we cannot say anything about its scalability.
※ordinary：ふつうの、ありふれた、一般的な。
「接続詞はなるべく使わないように」と「朱っ☆」（[3041]）されそうな文章が続きます。「interlocking systems guarantee the safety of trains at a station」することの「verifying」のための「a starting point」として…ゲフンゲフン。長すぎます。…として「the work presented in this thesis」は「successfully defined」したということです。そして、肝心の「What？」はといえば、「a method that uses ordinary station documentation」ということ…ですよね、たぶん。
> 12.2 Suggestions for future work
> （略）implementation relations should be proven in order to ensure the correctness of the concrete RSL model and the Java implementation.
> （略）one cannot know to which extent the size of the state space will constrain the verification of safety properties for larger stations.
> Therefore, it will be relevant to make a scalability study.
※ensure：保証する、one cannot know to 〜：〜が予想できない。
> The user-friendliness of the developed method can be improved in several ways.
> A tool for auto-generation of external behaviour and safety properties can be implemented.
> Also, it will be useful to develop a graphical user interface that is able to transform a graphical representation of diagrams to the XML format specified by this thesis and visualise counter-examples generated by the SAL model checker.
> One could also think of extending the Java implementation with an algorithm for simplifying the logical conditions for drawing and dropping relays. However, that might make the conditions less understandable for a human reader and it will not change the size of the state space.
※SAL model checker：「SA研」が提供しているモデル検証ツール（「the state-space based model checking tool SAL」）、counter-examples：反証（モデル検証ツールで弾かれた不正なモデル）。
「Aできる。Bできる。Cも考えられる。しかし、Cでは〜となってしまう。」と述べられています。カナシイかな、この順序で書かれますと、どうにもなかなかさようさよう、すんなりとは頭に入ってこないのは気のせいではないでしょう。
・Google Earth 「ordinary station」としての「Stenstrup Station」全景（南側から俯瞰）
https://goo.gl/maps/qo4vyw9XMjx
・Google ストリートビュー 最寄りの「Stenstrup Syd St.」付近
https://goo.gl/maps/LXZHFfg1ufA2
・Google ストリートビュー その南隣の「Svendborg Vest St.」付近
https://goo.gl/maps/WwEKCnB2PQU2
・Google ストリートビュー 北隣の「Kværndrup St.」付近
https://goo.gl/maps/Ei8WQXGbXrq
・（参考）「デンマーク工科大学における教育プログラムと学位授与概観」大学評価・学位研究 No.13（2012年3月）
http://www.niad.ac.jp/n_shuppan/gakujutsushi/mgzn13/no9_16_kadotad_no13_03.pdf
> 本稿は，ヨーロッパの中で最も成功した先駆的工学系大学の一つに数えられるデンマーク工科大学における工学教育と学位授与の現状を概観したものである。これは，日本の工学系大学院が今後進むべき方向性を見出すのに有益な情報を与えるものと考えられる。
> 日本の工学系大学院では，学位論文提出以前に予めそれを構成する主要部分に関する査読付論文を権威ある学術雑誌上に３編程度公表しておくことが義務付けられていることが多い。学術論文の公表を必須とする理由を教員が十分認識しているかどうか疑問であるが，論文投稿および厳しい査読の経験を積ませることが学生の能力と学位論文の質向上につながるというのが表向きの理由である。しかし，これが逆に学位の質低下を招く可能性がある。論文投稿および査読結果に対する対応などに多大な時間と労力を費やすため，学位論文作成に投入する時間と労力が減少することになる。また，論文数を気にしすぎるあまり，高度な内容の研究を行う代わりに，短期間にまとまる安直な研究を実施する可能性がある。
※とっても有益っぽいですが、今回は傍題です。（恐縮です。）
・「Automated Verification of Signalling Principles in Railway Interlocking Systems」（2009年）
http://cs.swan.ac.uk/~csfm/Pubs/entcs09.pdf
> Keywords: ladder logic, railway interlocking systems, SAT solvers, verification, automated theorem proving, signalling principles, safety properties.
とのことで、「SATソルバー」が出てきます。
・「私のブックマーク：SATソルバー」人工知能学会（2013年3月）
http://www.ai-gakkai.or.jp/my-bookmark_vol28-no2/
> 命題論理の充足可能性判定問題 (SAT) は，与えられた命題論理式の充足可能性を判定する問題であり，最初にNP完全性が証明された問題でもある．SATは人工知能および計算機工学における最も基本的な問題として，論理合成，システム検証，プランニング問題，スケジューリング問題，制約充足問題，制約最適化問題，定理証明など，さまざまな分野に応用されている．近年，106〜107個の変数をもつ大規模なSAT問題を，非常に高速に解くことが可能なSATソルバーが実現され，これらの分野への実用的応用が急速に拡大している．
「論理合成，システム検証，プランニング問題，スケジューリング問題，制約充足問題，制約最適化問題，定理証明など」を、（両極端として）▼「ワー！ 応用がいっぱい！」と読むか、▼「ぜんぶ同じことでしょ（充足可能性判定でしょ）」と読むかは分かれそうですが、そのどちらも、職務上の「お立場」しだい（ただし学生を含む）でありますから、排他の関係にはないといえましょう。
勉強や趣味でSATソルバーをば…といいますと「数独を解きましょう！」と一種「説かれ」るかとも思いますが、いえいえ、鉄道の連動装置を、駅単位でなく路線単位で、しかも時々刻々と運行に合わせて制約が変動していくという中、できれば車両基地も含めて全体で解きたいなどと考えていきますと、だいぶ大きな規模の問題になるんではないでしょうか＆本当でしょうか。
※こう、「編集部より鉄道に詳しいかた！」（[3226]）がたくさんいらしてですね、その、▼市販の時刻表、▼「JR貨物時刻表」、それに▼「鉄道ダイヤ情報」誌などを総合した上、さらに入出区のスジや検査の間隔など調べ尽くしてですよ、これはもう、ほとんど外形的には運行事業者と同じだけの情報を持っているわけですよ、たぶん。それだけツマビラカになっているなら、事業者に代わって『鉄道数独！』を解いてやろうという意欲的な人が、いまにも出てきそうだと思われてきます＆本当でしょうか。「模擬ヘラクレス」「模擬スピーディー」について[3089]も参照しながら、これを「カゴいっぱいのソフト！」（[3232]）…いえ「ゲーム」だと思って「名状しがたいフリーソフトのようなもの」など発表なさるだけで満足されてしまうのか、いやいやいや、大学院で研究にしあげるところまで持っていけるのか、仮には『レヴェルの高いソフト！』をうっかりつくってしまった人ほど、問われる（教員に引き留められる！）ことになっていきましょう。…などと、BVEのほう（[3089]）など眺めながらのうのうと（略）。レッツこれからは『若手』の時代だっ。
・藤田昌宏「SATアルゴリズムとその形式的検証への応用」（2006年12月5日）
http://www.cad.t.u-tokyo.ac.jp/fujita/SATDGFujita.pdf
前掲の人工知能学会の解説記事より長いスパン（1960年代から）で紹介されています。
・「仏ALCATEL社、制御システム(PLC制御プログラム)に対してモデル検査手法を適用」三菱総合研究所（2013年6月）
http://formal.mri.co.jp/news/2013/06/alcatelplc.html
> 旋盤のツールホルダータレットの制御のためのPLCプログラムについて、IEC61131-3で規定される5つの制御プログラム言語のうち、Ladder Diagram(LD), Sequentional Function Chart(SFC), Structured Text(ST)の言語を対象として、モデル検査システムCadence-SMVを適用した。
> 制御システムのPLCプログラムについては高い安全性、信頼性が要求されるため、フォーマルメソッドによる論理的な検証は、費用対効果の面で有効と考えられる。
・同（2010年12月1日）
http://formal.mri.co.jp/about.html
> ソフトウェアの正しさを論理的に検証し、その安全性や信頼性を確保するための方法として、形式手法に注目が集まっています。形式手法は、欧米では産業応用が進みつつありますが、国内では、一部の開発現場における適用にとどまり、開発現場への普及が進んでいません。
> 開発現場に普及しない理由として、形式手法の適用において必要となるモデリングやモデルの抽象化などに関する実践的な方法論が整備されていないことや、導入コストと効果の関係など意思決定者に必要な情報が見えていないことなどが挙げられます。
> 株式会社三菱総合研究所、日立ソリューションズ、株式会社ＮＴＴデータ、国立情報学研究所、北陸先端科学技術大学院大学は、2008年10月から、経済産業省の「新世代情報セキュリティ研究開発事業」により、形式手法の普及を妨げる問題を解決するために、情報家電等の実システムに対する形式手法適用のケーススタディを実施し、開発現場に形式手法を普及促進させるためのガイダンスの作成を開始しました。
書いてあること自体はなるほどですが、「普及が進む」ためには一種『上』だけがカシコクなるのでなく、開発現場全体が現状より数段、カシコクなっていかないと難しそうだ、と悲観されます。（あくまで個人ですが珍しく悲観します。）そのためには、研究所も含む「上」は、もっとカシコクなければなりません（「氷山の浮力」[2934]も参照）。
※「実践的な方法論」の「整備」を「口を開けて待っている！」（[3213]）ですと？ 取り組もうとしている課題の難易度と、取り組んでいただく『人材』に求めるソレとの一種「乖り！」が激しいのではないかとも感じられてきます。誰かが「実践的な方法論」を用意してくれるまで取り組めませーん、といっているレヴェルに留まる限り、「競争力」（[2934],[3282]）が云々などといっても…なんだかなぁ。かくして「誰かが本気出す」日は来るとしても「わたしが本気出す」日が来ることはないのではないか…などと（略）。
それはともかく、他人はともかく、自分は高みで、しかし遊ぶぞ〜、というと、よいツールはないでしょうか。
・「lp_solveを用いたNクイーン問題の解の探索」（2012年7月4日）
http://qiita.com/imos/items/fbdf8f300e68ebaca7b9
> Nクイーン問題のような問題は自分で探索プログラムを書くと探索空間が広くなりがちでなかなか解が見つけられなかったりします．そうでなくても書くのが面倒です．そういう時には線形計画法ソルバー(lp_solve)やSATソルバー(Sugar)などが便利です．
・田村直之ら「SAT型制約ソルバーSugarについて」（2011年1月31日）
http://bach.istc.kobe-u.ac.jp/papers/pdf/fpai2011slide.pdf
やっぱり数独で遊べと説かれます。ご興味ありましたら、ぜひお手元の環境で実際に実行されてみるとよいでしょう、たぶん。
| |
