定理自動証明技術の計算論的研究

1996 年度 実績報告書

• 研究課題/領域番号: 08044158
• 研究機関: 九州大学
• 研究代表者: 岩間 一雄 九州大学, 大学院・システム情報科学研究科, 教授 (50131272)
• 研究分担者: PAUL Purdom インディアナ大学, 計算機科学科, 教授 ; RUSSELL Impa カリフォルニア大学, サンジエゴ校・計算機科学科, 助教授 ; 桜井 幸一 九州大学, 大学院・システム情報科学研究科, 助教授 (60264066) ; TONIANN Pita アリゾナ大学, 計算機科学科, 助教授
• キーワード: 定理の自動証明 / 計算複雑さ / NP完全性 / SAT

研究概要

主要な研究活動は8年7月の代表者の米国訪問と、9年1月のPurdom博士の招聘による。なお、当初計画ではPitassi教授の招聘を考えていたが、同教授は8年8月にピッツバーグ大学からアリゾナ大学に異動し、日本訪問が不可能になった。
(1)代表者の米国訪問ではPitassi教授との討論を通して以下の成果を上げることができた。第一は、導出原理で定理を証明するときの計算複雑さを示す為の基本的アイデアを得たことである。第二は、Pitassi教授らが最近得た新しい結果と、この導出原理の複雑さの結果を合体させて、代表的NP完全問題である論理式の充足可能性問題の最悪計算時間を、現在までの指数時間から準指数時間へ減少させる方法に関する重大なヒントを得たことである。
(2)上記は充足不能な式の処理を目的としているが、充足可能な式の処理も同様に重要である。Purdom教授との討論ではバックトラック法で証明を行うときにいずれの変数を先に選択するべきかが効率改善に最重要であることを双方が確認した。
(3)なお、パ-ドム博士来日の機会を利用し、日本IBMの徳山博士、広島大学の新井博士、九州芸工大の岩本博士を交えて、「命題論理に対する複雑論的アプローチ」に関して集中討議を行った。この討議を通して新たに問題として提示された論理式の充足可能性問題の実用的応用に関する討論と資料収集の為代表者が東京と京都に出張する必要が生じたので、外国旅費の一部を国内旅費に流用した。

研究成果

• [文献書誌] 岩間,一雄: "α-connectivity : A gradually non-parallel graph problem" Journal of Algorithms. 20・3. 526-544 (1996)
• [文献書誌] 岩間,一雄: "Routing problems on the mesh of buses" Journal of Algorithms. 20・3. 613-631 (1996)
• [文献書誌] 岩間,一雄: "A faster parallel algorithm for κ-connecitivity" Proc.KOREA-JAPAN Joint Workshop on Algorithms and Computation. 8-13 (1996)
• [文献書誌] 櫻井,幸一: "A hidden cryptographic assumption in no-transferable identification schemes" Advances in Cryptology-Asiacrypt'96,Lecture Notes in Computer Science. (1996)
• [文献書誌] 岩間,一雄: "Database queries as combinatorial optimization problems" Proc.Int.Sympo.on Cooperative Database Systems for Advanced Applications. 448-454 (1996)
• [文献書誌] 岩間,一雄: "Random benchmark circuits with controlled attributes" European Design & Test Conference,ED & TC-97. (発表予定). (1997)
• [文献書誌] 岩間,一雄: "Adding new clauses for faster local search" Proc.13th National Conference on Artificial Intelligence. 304-310 (1996)
• [文献書誌] 岩間,一雄: "Oblivious Routing Algorithms on the Mesh of Buses" Proc.International Parallel Processing Symposium (IPPS'97). (発表予定). (1997)
• [文献書誌] 岩間,一雄: "Local search algorithms for partial MAXSAT" Proc.AAAI'97. (発表予定). (1997)
• [文献書誌] Pitassi,Toniann: "Simplified and improved resolution lower bounds" Proc.IEEE Symposium on Foundation of Computer Science. 274-282 (1996)
• [文献書誌] Impagliazzo,Russell: "Using the Groebner basis algorithm to find proofs of unsatisfiability" Proc.ACM Symposium on Theory of Computing. 174-183 (1996)
• [文献書誌] Purdom,Paul: "Backtracking and Probing" SIAM J.Comput.(発表予定). (1997)