講演抄録/キーワード |
講演名 |
2011-09-27 14:10
FPGAによるSAT問題のプリプロセッサの実現 ○鈴木将之・丸山 勉(筑波大) RECONF2011-40 |
抄録 |
(和) |
充足可能性問題(SAT 問題) は,論理式全体を真とするような変数への真偽の割り当てを求める問題である.回路検証やスケジューリングなど多くの問題がSAT に変換できるため,数多くのSAT ソルバが構築されてきた.しかし,SAT 問題はNP 完全であり,その計算量は非常に大きい.計算量を減らす一つの方法として,プリプロセッサによる問題規模の削減がある.本論文ではFPGA を用いたプリプロセッサ(SatELite) の構築について述べる.論理式中の項や節の依存関係を調べることにより項や節を削除することができ,問題の探索空間を小さくすることができる.SatELite で用いられているアルゴリズムは並列化しやすく,ハードウェア化に向いている.しかし,実際の回路から生成されたSAT 問題は,非常に規模が大きく,外部メモリとのデータ転送により,性能が制約される.本システムでは,FPGA 内にいくつかの節をキャッシュし,それらと他の節とを並列かつ連続的に比較する.また,比較された節は外部メモリのアクセス遅延を隠蔽するために再利用される.本システムの性能は問題規模に依存するが,大規模な問題では高い性能を達成した. |
(英) |
The satisfiability (SAT) problem is to find an assignment of binary values to the variables which satisfy a given clausal normal form (CNF). Many practical application problems can be transformed to SAT problems, and many SAT solvers have been developed. SAT problem is, however, NP-complete and its computational cost is very high. In order to reduce the computational cost, preprocessors are widely used by SAT solvers. In this paper, we describe an approach for implementing a preprocessor (SatELite) on FPGA. In SatELite, the variables and clauses whose values can be uniquely determined from other variables and clauses are eliminated to reduce the search space of the given SAT problem. The algorithms used in SatELite have inherent parallelism, but the data size of the SAT problems is very large, and the performance of the system is limited by the throughput of the o-chip DRAM banks. In our implementation, several clauses are held on the FPGA, and are compared in parallel with a sequence of new clauses. The sequence is cached on the FPGA, and reused in order to hide the access delay to the DRAM banks. The speedup by our system depends on the problem size, however it becomes higher for larger problems. |
キーワード |
(和) |
FPGA / SAT問題 / プリプロセッサ / / / / / |
(英) |
FPGA / SAT Problems / preprocessor / / / / / |
文献情報 |
信学技報, vol. 111, no. 218, RECONF2011-40, pp. 105-110, 2011年9月. |
資料番号 |
RECONF2011-40 |
発行日 |
2011-09-19 (RECONF) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
RECONF2011-40 |
研究会情報 |
研究会 |
RECONF |
開催期間 |
2011-09-26 - 2011-09-27 |
開催地(和) |
名古屋大学(NCES) |
開催地(英) |
Nagoya Univ. |
テーマ(和) |
リコンフィギャラブルシステム、一般 |
テーマ(英) |
Reconfigurable Systems, etc. |
講演論文情報の詳細 |
申込み研究会 |
RECONF |
会議コード |
2011-09-RECONF |
本文の言語 |
日本語 |
タイトル(和) |
FPGAによるSAT問題のプリプロセッサの実現 |
サブタイトル(和) |
|
タイトル(英) |
Variable and Clause Elimination in SAT problems using an FPGA |
サブタイトル(英) |
|
キーワード(1)(和/英) |
FPGA / FPGA |
キーワード(2)(和/英) |
SAT問題 / SAT Problems |
キーワード(3)(和/英) |
プリプロセッサ / preprocessor |
キーワード(4)(和/英) |
/ |
キーワード(5)(和/英) |
/ |
キーワード(6)(和/英) |
/ |
キーワード(7)(和/英) |
/ |
キーワード(8)(和/英) |
/ |
第1著者 氏名(和/英/ヨミ) |
鈴木 将之 / Masayuki Suzuki / スズキ マサユキ |
第1著者 所属(和/英) |
筑波大学 (略称: 筑波大)
University of Tsukuba (略称: Univ. of Tsukuba) |
第2著者 氏名(和/英/ヨミ) |
丸山 勉 / Tsutomu Maruyama / |
第2著者 所属(和/英) |
筑波大学 (略称: 筑波大)
University of Tsukuba (略称: Univ. of Tsukuba) |
第3著者 氏名(和/英/ヨミ) |
/ / |
第3著者 所属(和/英) |
(略称: )
(略称: ) |
第4著者 氏名(和/英/ヨミ) |
/ / |
第4著者 所属(和/英) |
(略称: )
(略称: ) |
第5著者 氏名(和/英/ヨミ) |
/ / |
第5著者 所属(和/英) |
(略称: )
(略称: ) |
第6著者 氏名(和/英/ヨミ) |
/ / |
第6著者 所属(和/英) |
(略称: )
(略称: ) |
第7著者 氏名(和/英/ヨミ) |
/ / |
第7著者 所属(和/英) |
(略称: )
(略称: ) |
第8著者 氏名(和/英/ヨミ) |
/ / |
第8著者 所属(和/英) |
(略称: )
(略称: ) |
第9著者 氏名(和/英/ヨミ) |
/ / |
第9著者 所属(和/英) |
(略称: )
(略称: ) |
第10著者 氏名(和/英/ヨミ) |
/ / |
第10著者 所属(和/英) |
(略称: )
(略称: ) |
第11著者 氏名(和/英/ヨミ) |
/ / |
第11著者 所属(和/英) |
(略称: )
(略称: ) |
第12著者 氏名(和/英/ヨミ) |
/ / |
第12著者 所属(和/英) |
(略称: )
(略称: ) |
第13著者 氏名(和/英/ヨミ) |
/ / |
第13著者 所属(和/英) |
(略称: )
(略称: ) |
第14著者 氏名(和/英/ヨミ) |
/ / |
第14著者 所属(和/英) |
(略称: )
(略称: ) |
第15著者 氏名(和/英/ヨミ) |
/ / |
第15著者 所属(和/英) |
(略称: )
(略称: ) |
第16著者 氏名(和/英/ヨミ) |
/ / |
第16著者 所属(和/英) |
(略称: )
(略称: ) |
第17著者 氏名(和/英/ヨミ) |
/ / |
第17著者 所属(和/英) |
(略称: )
(略称: ) |
第18著者 氏名(和/英/ヨミ) |
/ / |
第18著者 所属(和/英) |
(略称: )
(略称: ) |
第19著者 氏名(和/英/ヨミ) |
/ / |
第19著者 所属(和/英) |
(略称: )
(略称: ) |
第20著者 氏名(和/英/ヨミ) |
/ / |
第20著者 所属(和/英) |
(略称: )
(略称: ) |
講演者 |
第1著者 |
発表日時 |
2011-09-27 14:10:00 |
発表時間 |
25分 |
申込先研究会 |
RECONF |
資料番号 |
RECONF2011-40 |
巻番号(vol) |
vol.111 |
号番号(no) |
no.218 |
ページ範囲 |
pp.105-110 |
ページ数 |
6 |
発行日 |
2011-09-19 (RECONF) |
|