極小モデル生成とMaxSATソルバーについて
-
- 長谷川 隆三
- 九州大学大学院システム情報科学研究院情報学部門
Abstract
<p>モデル生成法とDPLL法の２つの証明手法の特徴を踏まえて、各手法による極小モデル生成 の実現法を紹介する。１階のモデル生成器MGTPを命題に特化したMiniMGとDPLL型SATソルバーMiniSATの性能比較を行う。制約充足問題は基数制約を付加してSAT問題に変換して解くことができる。代表的な基数制約の符号化方式Totalizerの改良版を提示し、MaxSAT問題を対象にその性能評価を行う。</p>
Journal
-
- Proceedings of the Annual Conference of JSAI
-
Proceedings of the Annual Conference of JSAI JSAI2014 (0), 1D4OS11a1-1D4OS11a1, 2014
The Japanese Society for Artificial Intelligence
- Tweet
Details 詳細情報について
-
- CRID
- 1390282763023113856
-
- NII Article ID
- 130007424369
-
- Text Lang
- ja
-
- Data Source
-
- JaLC
- CiNii Articles
-
- Abstract License Flag
- Disallowed