Solving satisfiability problems on FPGAs using experimental unit propagation

Takayuki Suyama, Makoto Yokoo, Akira Nagoya

研究成果: 著書/レポートタイプへの貢献会議での発言

3 引用 (Scopus)

抄録

This paper presents new results on an innovative approach for solving satisfiability problems (SAT), that is, creating a logic circuit that is specialized to solve each problem instance on Field Programmable Gate Arrays (FPGAs). This approach has become feasible due to recent advances in Reconfigurable Computing, and has opened up an exciting new research field in algorithm design. We have developed an algorithm that is suitable for a logic circuit implementation. This algorithm is basically equivalent to the Davis-Putnam procedure with Experimental Unit Propagation. The algorithm requires fewer hardware resources than previous approaches. Simulation results show that this method can solve a hard random 3-SAT problem with 400 variables within 1.6 minutes at a clock rate of 10MHz. Faster speeds can be obtained by increasing the clock rate. Furthermore, we have actually implemented a 128-variable, 256-clause problem instance on FPGAs.

元の言語英語
ホスト出版物のタイトルPrinciples and Practice of Constraint Programming – CP 1999 - 5th International Conference, CP 1999, Proceedings
編集者Joxan Jaffar
出版者Springer Verlag
ページ434-445
ページ数12
ISBN(印刷物)3540666265, 9783540666264
DOI
出版物ステータス出版済み - 1 1 1999
外部発表Yes
イベント5th International Conference on Principles and Practice of Constraint Programming, CP 1999 - Alexandria, 米国
継続期間: 10 11 199910 14 1999

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
1713
ISSN(印刷物)0302-9743
ISSN(電子版)1611-3349

その他

その他5th International Conference on Principles and Practice of Constraint Programming, CP 1999
米国
Alexandria
期間10/11/9910/14/99

Fingerprint

Satisfiability Problem
Field Programmable Gate Array
Field programmable gate arrays (FPGA)
Propagation
Unit
Logic circuits
Logic
Reconfigurable Computing
Clocks
Algorithm Design
Hardware
Resources
Simulation

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

これを引用

Suyama, T., Yokoo, M., & Nagoya, A. (1999). Solving satisfiability problems on FPGAs using experimental unit propagation. : J. Jaffar (版), Principles and Practice of Constraint Programming – CP 1999 - 5th International Conference, CP 1999, Proceedings (pp. 434-445). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 1713). Springer Verlag. https://doi.org/10.1007/978-3-540-48085-3_31

Solving satisfiability problems on FPGAs using experimental unit propagation. / Suyama, Takayuki; Yokoo, Makoto; Nagoya, Akira.

Principles and Practice of Constraint Programming – CP 1999 - 5th International Conference, CP 1999, Proceedings. 版 / Joxan Jaffar. Springer Verlag, 1999. p. 434-445 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻 1713).

研究成果: 著書/レポートタイプへの貢献会議での発言

Suyama, T, Yokoo, M & Nagoya, A 1999, Solving satisfiability problems on FPGAs using experimental unit propagation. : J Jaffar (版), Principles and Practice of Constraint Programming – CP 1999 - 5th International Conference, CP 1999, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 巻. 1713, Springer Verlag, pp. 434-445, 5th International Conference on Principles and Practice of Constraint Programming, CP 1999, Alexandria, 米国, 10/11/99. https://doi.org/10.1007/978-3-540-48085-3_31
Suyama T, Yokoo M, Nagoya A. Solving satisfiability problems on FPGAs using experimental unit propagation. : Jaffar J, 編集者, Principles and Practice of Constraint Programming – CP 1999 - 5th International Conference, CP 1999, Proceedings. Springer Verlag. 1999. p. 434-445. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-540-48085-3_31
Suyama, Takayuki ; Yokoo, Makoto ; Nagoya, Akira. / Solving satisfiability problems on FPGAs using experimental unit propagation. Principles and Practice of Constraint Programming – CP 1999 - 5th International Conference, CP 1999, Proceedings. 編集者 / Joxan Jaffar. Springer Verlag, 1999. pp. 434-445 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{a41c15b1348a4aa5b0fbcfaf54889043,
title = "Solving satisfiability problems on FPGAs using experimental unit propagation",
abstract = "This paper presents new results on an innovative approach for solving satisfiability problems (SAT), that is, creating a logic circuit that is specialized to solve each problem instance on Field Programmable Gate Arrays (FPGAs). This approach has become feasible due to recent advances in Reconfigurable Computing, and has opened up an exciting new research field in algorithm design. We have developed an algorithm that is suitable for a logic circuit implementation. This algorithm is basically equivalent to the Davis-Putnam procedure with Experimental Unit Propagation. The algorithm requires fewer hardware resources than previous approaches. Simulation results show that this method can solve a hard random 3-SAT problem with 400 variables within 1.6 minutes at a clock rate of 10MHz. Faster speeds can be obtained by increasing the clock rate. Furthermore, we have actually implemented a 128-variable, 256-clause problem instance on FPGAs.",
author = "Takayuki Suyama and Makoto Yokoo and Akira Nagoya",
year = "1999",
month = "1",
day = "1",
doi = "10.1007/978-3-540-48085-3_31",
language = "English",
isbn = "3540666265",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "434--445",
editor = "Joxan Jaffar",
booktitle = "Principles and Practice of Constraint Programming – CP 1999 - 5th International Conference, CP 1999, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Solving satisfiability problems on FPGAs using experimental unit propagation

AU - Suyama, Takayuki

AU - Yokoo, Makoto

AU - Nagoya, Akira

PY - 1999/1/1

Y1 - 1999/1/1

N2 - This paper presents new results on an innovative approach for solving satisfiability problems (SAT), that is, creating a logic circuit that is specialized to solve each problem instance on Field Programmable Gate Arrays (FPGAs). This approach has become feasible due to recent advances in Reconfigurable Computing, and has opened up an exciting new research field in algorithm design. We have developed an algorithm that is suitable for a logic circuit implementation. This algorithm is basically equivalent to the Davis-Putnam procedure with Experimental Unit Propagation. The algorithm requires fewer hardware resources than previous approaches. Simulation results show that this method can solve a hard random 3-SAT problem with 400 variables within 1.6 minutes at a clock rate of 10MHz. Faster speeds can be obtained by increasing the clock rate. Furthermore, we have actually implemented a 128-variable, 256-clause problem instance on FPGAs.

AB - This paper presents new results on an innovative approach for solving satisfiability problems (SAT), that is, creating a logic circuit that is specialized to solve each problem instance on Field Programmable Gate Arrays (FPGAs). This approach has become feasible due to recent advances in Reconfigurable Computing, and has opened up an exciting new research field in algorithm design. We have developed an algorithm that is suitable for a logic circuit implementation. This algorithm is basically equivalent to the Davis-Putnam procedure with Experimental Unit Propagation. The algorithm requires fewer hardware resources than previous approaches. Simulation results show that this method can solve a hard random 3-SAT problem with 400 variables within 1.6 minutes at a clock rate of 10MHz. Faster speeds can be obtained by increasing the clock rate. Furthermore, we have actually implemented a 128-variable, 256-clause problem instance on FPGAs.

UR - http://www.scopus.com/inward/record.url?scp=84957367729&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84957367729&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-48085-3_31

DO - 10.1007/978-3-540-48085-3_31

M3 - Conference contribution

SN - 3540666265

SN - 9783540666264

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 434

EP - 445

BT - Principles and Practice of Constraint Programming – CP 1999 - 5th International Conference, CP 1999, Proceedings

A2 - Jaffar, Joxan

PB - Springer Verlag

ER -