| 研究概要 |
命題論理の充足可能性問題(SAT)は,計算機科学におけるもっとも重要な問題のひとつである.我々はSATに対して,LPPHと呼ばれる力学系を提案し,この力学系を用いることにより効率良く解を求めることができることを,理論的,実験的に証明している.本研究では,この与えられたCNFの各節に注目度と呼ばれる係数を導入し解を求める時間のさらなる短縮を計ること,および,問題と共に予備的な解が与えられた時にその予備解に対応する方法についての研究を行った.
これまでの研究により,グローバルな解(SATの解)への収束性に関しては,力学系の減衰係数が大きく関与していることが分かっている.減衰率によりCNFの各節への重点の置き方をダイナミックに調節していると考えられる.本研究では,各節への重点の置き方を各節に対する注目度とみなし,注目度を制御することにより解を求める時間を短縮する手法を開発した.この手法では,充足が困難である節の組み合わせを見つけ,その組み合わせに注目し,力学系LPPHにおいて充足させるような力を重点的に働かせることにより,効率良く解を探索しようとする.実験の結果,従来解くのが困難であった問題ほど,より効果が高いことが実証された.
予備的な解は,「解はこのようになりそうだよ」というヒントや,「このような解がほしい」という解に対する要求として与えられる.前者の場合は,予備解を有効に利用して解を求める時間の短縮を計ることが,後者の場合は,より予備解に近い解が要求される.一般に予備解には,不正確さやあいまいさが含まれる.本研究では,力学系LPPHにおいて,バイアス項を導入することにより,これらの2つの型の予備解に対応する方法を提案した.従来のSATを解く手法に対しても,これらの予備解に対応する手法を作成し,比較実験を行った結果,LPPHの方が有効であることが分かった.
|
