論理方程式に対する計数方による解法とその応用に関する研究

点击翻译按钮获取中文摘要

本年度の研究目標として、(1)計数法の実用性の検証及びその結果に基づくアルゴリズムの改良、(2)実際的問題への応用の2点をあげた。(1)米国インジアナ大学のPurdom教授が、理論式の充足可能性判定問題を解く代表的な数個のアルゴリズムのランダム入力に対する性能評価を計算機実験によって行い、代表者も米国を訪問し協力した。その結果によれば、計数法は与えられたCNF理論式の各項にリテラルが比較的多く現れるような(かなり大きな)クラスに対しては他のアルゴリズムより圧倒的にすぐれていることが確認された。Iwama's Algorithmとして世界的に浸透しつつある。現在この解析結果に基づき実用性を上げる方向での改良を進めている。他のアルゴリズムと組み合わせて互いの利点を引き出すことが可能であり、上記Purdom教授との協同研究を計画中である。計数法自体の改良の可能性もいくつか指摘されており、特に、計算の早期打切りを可能にする発見的手法の導入が有力視されている。その効果を確かめる為の数学的解析を現在進めておりまもなく結果を公表する予定である。(2)結め将棋を解くプログラムの開発を学生の協力を得て行い、そのような実際的問題で論理方程式を解く必要が生じる場面がどの程度現れるか検討した。プログラム自体は十数手結の問題まで実用的時間で解けるものが完成している。論理方程式を解くことによって解探索の空間を縮小することができるが同時にプログラミングの手間が予想以上に大きいものであることが判明した。ゲ-ム木の総当り的探索に比べどの程度有利であるかの定量的解析を試みている。