ＳＡＴ符号化を用いた釣合い型不完備ブロック計画の構成

• 松中 春樹

  神戸大学 大学院システム情報学研究科

• 丹生 智也

  神戸大学 大学院工学研究科

• 番原 睦則

  神戸大学 情報基盤センター

• 田村 直之

  神戸大学 情報基盤センター

書誌事項

タイトル別名

• Generating Balanced Incomplete Block Designs by SAT Encoding

抄録

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.

収録刊行物

• 人工知能学会論文誌

  人工知能学会論文誌 27 (2), 10-15, 2012

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

キーワード

• propositional satisfiability (SAT)
• SAT encoding
• balanced incomplete block design (BIBD)

詳細情報

• CRID: 1390001205107781376
• NII論文ID: 130001878739
• DOI: 10.1527/tjsai.27.10
• ISSN: 13468030
• ISSN: 13460714
• HANDLE: 20.500.14094/90002837
• Web Site: http://www.jstage.jst.go.jp/article/tjsai/27/2/27_2_10/_pdf
• 本文言語コード: ja
• データソース種別:
  • JaLC
  • IRDB
  • Crossref
  • CiNii Articles
  • KAKEN
• 抄録ライセンスフラグ: 使用不可