2014 Fiscal Year Research-status Report
「証明問題＋推論」から「求解問題＋等価変換」への大転換
| Project/Area Number |
26540110
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
赤間 清 北海道大学, 情報基盤センター, 特任教授 (50126265)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | 求解問題 / 証明問題 / 推論 / 等価変換 / スコーレム化 / 意味保存スコーレム化 / 関数変数 / 論理構造 |
|---|
| Outline of Annual Research Achievements |
1. 問題変換システムの整備、構造化、拡張を行った。いくつかの問題をいろいろな経路で解くことによって、いくつかの重要な等価変換が発見できた。たとえば、サイドチェンジ変換、独立充足可能アトム列の除去変換、フォワード変換などである。
2. 一階述語論理式から節形式に変換するアルゴリズム（意味保存スコーレム化を含む変換）を改めて定式化し、その正当性と停止性を厳密に証明した。
3. モデル全体の集合を保存すれば、求解問題の解は保存される。本研究ではこれを拡張して、目標写像という概念を導入し、目標写像を保存する変換はすべて、求解問題の解を保存することを証明した。これは等価変換ルールの可能性を拡大する。いくつかの有用な目標写像の候補を提案し、それが実際に目標写像であることを証明した。たとえば、任意の節集合に対して、ボトムアップ計算で得られる集合を対応させる写像は目標写像を構成する。それは有限集合の場合もあれば、無限集合の場合もある。目標写像を用いて、いくつかの変換ルールが等価変換ルールであることが証明できた。
4. 上記の理論に基づいて、SATソルバーによる問題解決を等価変換による解法の部品として位置付けた。すなわち、SATソルバーの入力をつくるために節集合をグラウンドな有限節集合に落とす計算は等価変換であり、SATソルバーは目標写像の１つの例であることを証明した。これはSATソルバーの入力をどう作ればいいかという理論的問題を解決する。すなわち、等価変換によってSATソルバーの入力にあたるグラウンドな節集合までたどりつけばよい。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
問題変換システムの構築と実験では、問題変換システムの整備、構造化、拡張を行った。実験により、いくつかの重要な等価変換ルールが発見できた。一階述語論理式から節形式に変換するアルゴリズムの正当性と停止性を証明した。これは証明問題や求解問題の解を求める際に最初に適用しなければならない重要なアルゴリズムである。求解問題を解くカギである目標写像を発見し、いくつかの有用な目標写像を提案した。これは多様な求解問題の解法に貢献する。求解問題を解く枠組みは、より一般的な枠組みへと発展中である。このように重要な概念が革新され、理論的枠組みが発展し、障害が見当たらないので、おおむね順調に進展しているといえる。
|
| Strategy for Future Research Activity |
求解問題の一般クラスの定式化と等価変換による解法の理論を完成する。求解問題の一般クラスとは、特殊化システムをパラメータとする論理構造に基づく問題クラスであり、特殊化システムを具体的に指定することにより、いろいろなデータ構造を持つ領域に適用できる。この一般クラスに対して等価変換による解法を定式化し、解の正当性を証明すれば、それは非常に多くの領域で等価変換による解法が有効であることを意味する。また等価変換に基づく解法が問題構造から見て本質的な解法であることを明確に示すことになる。これはきわめて重要なので、次年度の最重要課題として設定する。
|
| Causes of Carryover |
平成２６年度の３月に実施した出張の旅費が平成２７年度に支出されたため、68,880円の次年度使用額が生じた。その他の次年度使用額は人件費の利用が難しかったなどの理由により生じた。
|
| Expenditure Plan for Carryover Budget |
平成２６年度３月に実施した出張の旅費が平成２７年度に支出されたため生じた次年度使用額については、当該出張旅費の支出に充てる。その他の次年度使用額は、旅費や国際会議参加費として利用する。
|
