著者

松中 春樹 丹生 智也 番原 睦則 田村 直之

出版者

一般社団法人 人工知能学会

雑誌

人工知能学会論文誌 (ISSN:13460714)

巻号頁・発行日

vol.27, no.2, pp.10-15, 2012 (Released:2012-01-13)

参考文献数

15

---

Propositional Satisfiability (SAT) is fundamental in solving many application problems in Artificial Intelligence and Computer Science. Remarkable improvements in the efficiency of SAT solvers have beenmade over the last decade. Such improvements encourage researchers to solve constraint satisfaction problems by encoding them into SAT (i.e. ``SAT encoding''). Balanced Incomplete Block Design (BIBD) is one of the most typical block designs. BIBDs have been applied in several fields such as design experiments, coding theory, and cryptography. In this paper, we consider the problem of generating BIBDs by SAT encoding. We present a new SAT encoding that is an enhancement of order encoding with the idea of binary tree. It is designed to reduce the number of clauses required for cardinality constraints, compared with order encoding. In our experiments, our encoding was able to give a greater number of solutions than order encoding and state-of-the-art constraint solvers Mistral and choco.