充足可能性問題の0-1整数計画問題への定式化と計算効率

情報処理学会

書誌事項

タイトル別名
  • Transformation of SAT into Zero-one Integer Programming Problem

この論文をさがす

説明

命題論理や第一階述語論理の充足可能性問題(SAT)は,情報科学の基本的な問題の一つであり,現在まで多くの研究が行われている.それらの研究は,Robinsonの導出原理に基づく方法とOR技法の一つである0-1整数計画法(0-1IP)を適用する方法に大別できる.これら2つのアプローチに共通する前提は,一般にSATが節形式で与えられることである.本論文では,命題論理のSATを節形式に変換せずに,直接0-1IP問題に変換するアルゴリズムを示す.そして,SATの充足可能性と0-1IP問題の整数制約を除き連続緩和した問題(LR問題)の解の間の関係を明らかにする.さらに,節形式に対するDavis-PutnamのアルゴリズムとLR問題を解く線形計画法の関係を示す.

収録刊行物

  • 全国大会講演論文集

    全国大会講演論文集 第44回 (人工知能及び認知科学), 13-14, 1992-02-24

    情報処理学会

詳細情報 詳細情報について

問題の指摘

ページトップへ