人工知能学会研究会資料 人工知能基本問題研究会
Online ISSN : 2436-4584
97回 (2014/3)
会議情報

制約充足問題のハイブリッド符号化に向けて
宋 剛秀佐古田 淳史番原 睦則田村 直之
著者情報
会議録・要旨集 フリー

p. 12-

詳細
抄録

In this paper, we propose a hybrid encoding of Constraint Satisfaction Problems (CSPs) to propositional logic (especially SAT and PB). There have been proposed several encodings of CSPs to propositional logic, such as direct encoding, order encoding, and binary encoding. However, each of these encodings has its pros and cons. For example, the order encoding which is used in a SAT-based constraint solver Sugar, showed a good performance on many problem instances, but it can not be applied to CSP instances with very large domain size. On the other hand, the binary encoding is applicable to those large instances, but the generated SAT instances take more time to be solved than the order encoded instances in general. The hybrid encoding proposed in this paper mixes the order and binary encodings so that it can be applied to very large instances while it keeps the good performance of the order encoding for small instances. We evaluated the performance of the proposed hybrid encoding with our implementation named Hysca. In our evaluation using 1453 instances of the 2009 CSP solver competition, Hysca succeeded to solve 1075 instances, which is 56 more than the order encoding, and 53 more than the binary encoding.

著者関連情報
© 2015 人工知能学会
前の記事 次の記事
feedback
Top