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

• Item type: Journal(1)
• 公開日: 1993-12-15
• タイトル: 陰的列挙法に基づくSATアルゴリズム
• タイトル / 言語: en
• タイトル: SAT Algorithm Based on Implicit Enumeration Method
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• その他タイトル / その他のタイトル: 探索アルゴリズム
• 著者所属: 札幌医科大学保健医療学部
• 著者所属: 北海道大学工学部情報工学科
• 著者所属: 北海道大学工学部情報工学科
• 著者所属(英): en
• 著者所属(英): School of Health Sciences, Sapporo Medical University
• 著者所属(英): en
• 著者所属(英): Department of Information Engineering, Faculty of Engineering, Hokkaido University
• 著者所属(英): en
• 著者所属(英): Department of Information Engineering, Faculty of Engineering, Hokkaido University
• 著者名: 大柳, 俊夫; 山本, 雅人; 大内, 東
• 著者名(英): Toshio, Ohyanagi; Masahito, Yamamoto; Azuma, Ohuchi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 命題論理の充足可能性問題（以下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の有効性を検証する。
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 34, 号 12, p. 2464-2473, 発行日 1993-12-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764