お知らせ 2023年度・2024年度 学生員 会費割引キャンペーン実施中です
お知らせ 技術研究報告と和文論文誌Cの同時投稿施策(掲載料1割引き)について
お知らせ 電子情報通信学会における研究会開催について
お知らせ NEW 参加費の返金について
電子情報通信学会 研究会発表申込システム
講演論文 詳細
技報閲覧サービス
[ログイン]
技報アーカイブ
 トップに戻る 前のページに戻る   [Japanese] / [English] 

講演抄録/キーワード
講演名 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 
ページ数
発行日 2011-09-19 (RECONF) 


[研究会発表申込システムのトップページに戻る]

[電子情報通信学会ホームページ]


IEICE / 電子情報通信学会