命題論理充足可能性問題に対する定量的アプローチと記号的アプローチの比較

概要

論文の詳細を見る
命題論理の充足可能問題(SAT)は,情報処理の分野における基本的な問題の一つで,現在まで多くの研究が行われている.それらの研究は,Robinsonの導出原理に基づく記号的アプローチと,OR技法の一つである0-1整数計画法に基づく定量的アプローチに大別できるこれまでの記号的アプローチと定量的アプローチの関係に関する研究は,Dzvis-Putnam(DP)の方法と0-1整数計画法の対応,導出節と0-1整数計画法のカットの密接な関係,などの倫理的な議論と,計算機上の数値実験として,DPと分枝限定法および切除平面法との比較など行なわれている.しかし,記号的アプローチの中で最も有効と考えられるホーン緩和戦略と整数計画法の比較や,整数計画法のアルゴリズムのSAT向きの見直しなどはほとんど行われていない.最近著者らは,定量的アプローチの1つとして0-1整数計画問題に対する陰的列挙法をSAT向きに改訂した改訂陰的列挙法を提案している.本稿では,著者らが考案した改訂陰的列挙法の概略とそのインプリメンテーション方法について述べる.そして,改訂陰的列挙法とホーン緩和戦略の比較実験をランダム3-SATを用いて行った結果について報告する.
一般社団法人情報処理学会の論文
1992-09-28