WEKO3
アイテム
SATに対する局所探索法のベクトル化
https://ipsj.ixsq.nii.ac.jp/records/12006
https://ipsj.ixsq.nii.ac.jp/records/12006462c4b23-367d-4c58-803f-be0376d07746
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-JNL4204012.pdf (410.7 kB)
|
Copyright (c) 2001 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Journal(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2001-04-15 | |||||||
| タイトル | ||||||||
| タイトル | SATに対する局所探索法のベクトル化 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Vectorized Local Search for CNF Satisfiability | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 特集：並列処理 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| その他タイトル | ||||||||
| その他のタイトル | 並列アルゴリズム | |||||||
| 著者所属 | ||||||||
| 豊田自動織機製作所 | ||||||||
| 著者所属 | ||||||||
| 京都大学情報学研究科 | ||||||||
| 著者所属 | ||||||||
| 京都大学情報学研究科 | ||||||||
| 著者所属 | ||||||||
| 京都大学情報学研究科 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Toyoda Automatic Loom Works Ltd. | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Informatics, Kyoto University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Informatics, Kyoto University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Informatics, Kyoto University | ||||||||
| 著者名 |
河合, 大輔
× 河合, 大輔
|
|||||||
| 著者名(英) |
Daisuke, Kawai
× Daisuke, Kawai
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 本研究の目的は，和積形論理式の充足可能性問題（SAT）の解法アルゴリズムである局所探索法の高速化である．局所探索法のアルゴリズムGSATに対し，実働化時の工夫と並列化によって高速化を試みる．SelmanとKautzのGSATを元に，(i)~データ構造の改良，(ii)~ベクトル並列計算機上でのベクトル化，(iii)~PVMを使った40? CPUによる並列化，を行った．これにより，合計600倍の高速化を達成した．2nd DIMACS Implementation Challenge Satisfiabilityのベンチマーク例題に対して我々のGSATを実行させたところ，既存のプログラムで解けている例題では実行時間がかなり短縮された．また，GSATを改良した局所探索法に本論文の手法を適用させることにより，既存のプログラムでは解けなかった例題を解くまでに至った． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | The purpose of this paper is to speed up the local search algorithmfor CNF Satisfiability problem by implementation techniques andparallelization. We selected GSAT by Selman and Kautz and attemptedspeedup by the following techniques: (i)~An improvement of the datastructure of Selman and Kautz's implementation. (ii)~Vectorization ona parallel vector supercomputer. (iii)~Parallelization using ParallelVirtual Machine (PVM). By these attempts, we achieved 600-timesspeedup in total. We executed our GSAT for benchmark instances of the2nd DIMACS Implementation Challenge, Satisfiability. Our programperformed much better than existing programs on most instances.Moreover, we were able to solve some instances that existing programscould not have solved. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AN00116647 | |||||||
| 書誌情報 |
情報処理学会論文誌 巻 42, 号 4, p. 754-761, 発行日 2001-04-15 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7764 | |||||||
