Proposal and Evaluation of Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings

DOI HANDLE Web Site 被引用文献1件 参考文献14件 オープンアクセス

抄録

This paper proposes a new hybrid encoding of finite linear CSP to SAT which integrates order and log encodings. The former maintains bound consistency by unit propagation and works well for constraints consisting of small/middle sized arity and variable domains. The latter generates smaller CNF and works well for constraints consisting of larger sized arity and variable domains but its performance is not good in general because more inference steps are required to ripple carries. This paper describes the first attempt of hybridizing the order and log encodings without channeling constraints. Each variable is encoded by either the order encoding or the log encoding, and each constraint can contain both types of variables. Using the CSP solver competition benchmark consisting of 1458 instances, we made a comparison between the order, log and proposed hybrid encodings. As a result, the hybrid encoding solves the largest number of instances with the shortest CPU time. We also made a comparison with the four state-of-the-art CSP and SMT solvers Mistral, Opturion CPX, Yices, and z3. In this comparison, the hybrid encoding also shows the best performance. Furthermore, we found that the hybrid encoding is especially superior than other solvers for instances containing disjunctive constraints and global constraints — it indeed solves more instances than the virtual best solver consisting of those four state-of-the-art systems.

収録刊行物

被引用文献 (1)*注記

もっと見る

参考文献 (14)*注記

もっと見る

関連プロジェクト

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ