神戸大学附属図書館デジタルアーカイブ
入力補助
English
カテゴリ
学内刊行物
ランキング
アクセスランキング
ダウンロードランキング
https://hdl.handle.net/20.500.14094/90004656
このアイテムのアクセス数:
31
件
(
2024-04-26
14:47 集計
)
閲覧可能ファイル
ファイル
フォーマット
サイズ
閲覧回数
説明
90004656 (fulltext)
pdf
481 KB
16
メタデータ
ファイル出力
メタデータID
90004656
アクセス権
open access
出版タイプ
Accepted Manuscript
タイトル
Proposal and Evaluation of Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings
著者
Soh, Takehide ; Banbara, Mutsunori ; Tamura, Naoyuki
著者ID
A0011
研究者ID
1000000625121
KUID
https://kuid-rm-web.ofc.kobe-u.ac.jp/search/detail?systemId=be19a5fd36bdbe87520e17560c007669
著者名
Soh, Takehide
宋, 剛秀
ソウ, タケヒデ
所属機関名
情報基盤センター
著者ID
A1730
研究者ID
1000080290774
著者名
Banbara, Mutsunori
番原, 睦則
バンバラ, ムツノリ
所属機関名
情報基盤センター
著者ID
A0899
研究者ID
1000060207248
KUID
https://kuid-rm-web.ofc.kobe-u.ac.jp/search/detail?systemId=64672be7ad29e33a520e17560c007669
著者名
Tamura, Naoyuki
田村, 直之
タムラ, ナオユキ
所属機関名
情報基盤センター
収録物名
International Journal on Artificial Intelligence Tools
巻(号)
26(1)
ページ
1760005-1760005
出版者
World Scientific Publishing
刊行日
2017-02
公開日
2018-03-05
抄録
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.
キーワード
Order encoding
log encoding
hybrid
カテゴリ
情報基盤センター
学術雑誌論文
権利
© World Scientific Publishing Company. Electronic version of an article published as International Journal on Artificial Intelligence Tools 26, 1, 2017, 1760005. DOI: 10.1142/S0218213017600053, http://www.worldscientific.com/worldscinet/ijait
詳細を表示
資源タイプ
journal article
言語
English (英語)
ISSN
0218-2130
OPACで所蔵を検索
CiNiiで学外所蔵を検索
eISSN
1793-6349
OPACで所蔵を検索
CiNiiで学外所蔵を検索
関連情報
DOI
https://doi.org/10.1142/S0218213017600053
ホームへ戻る