陰的列挙法に基づくSATアルゴリズム

• 大柳, 俊夫

• 山本, 雅人

• 大内, 東

書誌事項

タイトル別名

• SAT Algorithm Based on Implicit Enumeration Method

抄録

命題論理の充足可能性問題（以下SATと呼ぷ）は、計算複雑度がNP一完全である代表的な問題として、情報処理の分野における墓本酌な問題の一つにあげられている。この問題に対して、Davis-Putnamの方法に代表される記号的方法に関する研究がこれまで盛んに行われている。最近になって、OR技法の一つである整数計画法や線形計画法に基づく研究が主にORの分野の研究者によって行われている。この方法は記号的方法に対し定量的方法と呼ばれ、本来計算機が得意とする数値的な処理によりSATを高遠に解くことを目指したものである。SATに対する定量的方法に関するこれまでの研究として、1）Branch and Broundに基づく方法、2）切除平面に基づく方法、3）内点法に基づく方法、4）陰的列挙法に基づく方法、などが提案されている。本論文では、陰的列挙法に基づく新しいSATアルゴリズムIEMSATを提案する。そして、SATに対する代表的な方法であるDavis?Putnamと提案アルゴリズムの関係を詳細に調べ両方法の対応付けを行う。この結果は、一般のO-１整数計画問題に対する陰的列挙法をSAT向きに特殊化することで、Davis・Putnamとほぽ同じ方法が導げることを示すものである。また、IEMSAT為よびDavis?Putnamの方法を用いた計算機実験を行い、IEMSATの有効性を検証する。

収録刊行物

• 情報処理学会論文誌

  情報処理学会論文誌 34 (12), 2464-2473, 1993-12-15

  一般社団法人情報処理学会

キーワード

• 論文

詳細情報

• CRID: 1050001339022781184
• NII論文ID: 110002722617
• NII書誌ID: AN00116647
• HANDLE: 2115/64520
• ISSN: 18827764
• Web Site: http://id.nii.ac.jp/1001/00014322/
• 本文言語コード: ja
• 資料種別: journal article
• データソース種別:
  • IRDB
  • CiNii Articles