The 28th Annual Conference of the Japanese Society for Artificial Intelligence, 2014
1D4-OS-11a-1
極小モデル生成と
MaxSAT
ソルバーについて
On Minimal Model Generation and MaxSAT Solver
長谷川
隆三
∗1Ryuzo Hasegawa
∗1
九州大学大学院システム情報科学研究院
Faculty of Information Science and Electrical Engineering, Kyushu University
We present an implementation method of minimal model generation based on consideration on features of model generation method and DPLL (Davis Putnam Logemann Loveland) procedure. We give a performance comparison of MiniMG and MiniSAT solvers. The former is obtained by specializing a first order theorem prover MGTP to solve propositional one. The latter is a SAT solver based on DPLL. Several constraints satisfaction problems contain cardinality constraints. Solving such problems with SAT solvers requires SAT encodings for cardinality constraints. We introduce Modulo Totalizer, a modification of Totalizer which is a well known SAT encoding of cardinality constraints, and evaluate its performance by solving MaxSAT instances.
謝辞 本研究の一部は科研費（20240003，21300054，25330085，
25330262）の助成を受けたものです．
参考文献
[1] Roberto As´ın, Robert Nieuwenhuis, and Albert Oliv-eras. Cardinality Networks: a theoretical and empirical study. Constraints, 16:195–221, 2011.
[2] Olivier Bailleux and Yacine Boufkhad. Efficient CNF Encoding of Boolean Cardinality Constraints. In Pro-ceedings of 9th International Conference on Principles and Practice of Constraint Programming (CP 2003), pages 108–122, 2003.
[3] Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability. IOS Press, 2009.
[4] Niklas E´en and Niklas S¨orensson. An Extensible SAT-solver. InProceedings of 6th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), pages 502–518, 2003.
[5] Ryuzo Hasegawa, Hiroshi Fujita, and Miyuki Koshimura. MGTP: A Model Generation Theorem Prover - Its Advanced Features and Applications. In
Proceedings of International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX ’97), pages 1–15, 1997.
[6] Ryuzo Hasegawa, Hiroshi Fujita, and Miyuki Koshimura. Efficient Minimal Model Generation Us-ing BranchUs-ing Lemmas.. InProceedings of 17th Inter-national Conference on Automated Deduction(CADE 2000), pages 184–199, 2000.
連絡先: 長谷川隆三，九州大学大学院システム情報科学研究
院，〒819-0395福岡市西区元岡744，092-802-3608
[7] Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, and Ryuzo Hasegawa. QMaxSAT: A Partial Max-SAT Solver.Journal on Satisfiability, Boolean Modeling and Computation, 8:95–100, 2012.
[8] Chu Min Li and Felip Many`a.MaxSAT, Hard and Soft Constraints, chapter 19, pages 613–631. In Biere et al. [3], 2009.
[9] Toru Ogawa, YangYang Liu, Ryuzo Hasegawa, Miyuki Koshimura, and Hiroshi Fujita. Modulo Based CNF Encoding of Cardinality Constraints and Its Applica-tion to MaxSAT Solvers. InProceedings of IEEE 25th International Conference on Tools with Artificial In-telligence (ICTAI 2013), pages 9–17, 2013.
[10] Olivier Roussel and Vasco Manquinho. Pseudo-Boolean and Cardinality Constraints, chapter 22, pages 695–733. In Biere et al. [3], 2009.
[11] Joost P. Warners. A linear-time transformation of lin-ear inequalities into conjunctive normal form. Infor-mation Processing Letters, 68:63–69, 1998.
[12] 小川 徹，劉 洋洋，長谷川 隆三，越村 三幸，藤田 博．
Modulo計算に基づく基数制約のCNF符号化方式の提 案と評価.九州大学システム情報科学紀要, 18(2):85–92,
2013.
[13] 佐々木佑介． モデル生成型SATソルバーにおける学習
節の分岐利用判定手法と削除戦略について. 九州大学大
