FPGAによるSAT問題のプリプロセッサの実現

• Item type: Journal(1)
• 公開日: 2016-01-15
• タイトル: FPGAによるSAT問題のプリプロセッサの実現
• タイトル / 言語: en
• タイトル: Variable and Clause Elimination in SAT Problems Using an FPGA
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [一般論文] SAT問題，プリプロセッサ，FPGA，アクセラレータ
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 筑波大学
• 著者所属: 筑波大学
• 著者所属(英): en
• 著者所属(英): University of Tsukuba
• 著者所属(英): en
• 著者所属(英): University of Tsukuba
• 著者名: 鈴木, 将之; 丸山, 勉
• 著者名(英): Masayuki, Suzuki; Tsutomu, Maruyama
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 充足可能性問題（SAT問題）は，論理式全体を真とするような変数への真偽の割当てを求める問題である．スケジューリングや回路検証など多くの問題がSATに変換できるため，数多くのSATソルバが構築されてきた．しかし，SAT問題はNP完全であり，その計算量は非常に大きい．計算量を減らす1つの方法として，プリプロセッサによる問題規模の削減がある．本論文ではFPGAを用いたプリプロセッサ（SatELite）の構築について述べる．論理式中の項や節の依存関係を調べることにより項や節を削除することができ，問題の探索空間を小さくすることができる．SatELiteで用いられているアルゴリズムは並列化しやすく，ハードウェア化に向いている．しかし，実際の回路から生成されたSAT問題は，非常に規模が大きく，外部メモリとのデータ転送により，性能が制約される．本システムでは，FPGA内にいくつかの節をキャッシュし，それらと他の節とを並列かつ連続的に比較する．また，比較された節は外部メモリのアクセス遅延を隠蔽するために再利用される．本システムの性能は問題規模に依存するが，大規模な問題においては高い高速化を達成することができた．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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 in 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 off-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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 57, 号 1, p. 343-352, 発行日 2016-01-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764