Solving satisfiability problems on FPGAs using experimental unit propagation

Takayuki Suyama; Makoto Yokoo; Akira Nagoya

doi:10.1007/978-3-540-48085-3_31

Solving satisfiability problems on FPGAs using experimental unit propagation

Takayuki Suyama, Makoto Yokoo, Akira Nagoya

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

3 Citations (Scopus)

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.

Original language	English
Title of host publication	Principles and Practice of Constraint Programming – CP 1999 - 5th International Conference, CP 1999, Proceedings
Editors	Joxan Jaffar
Publisher	Springer Verlag
Pages	434-445
Number of pages	12
ISBN (Print)	3540666265, 9783540666264
DOIs	https://doi.org/10.1007/978-3-540-48085-3_31
Publication status	Published - 1999
Externally published	Yes
Event	5th International Conference on Principles and Practice of Constraint Programming, CP 1999 - Alexandria, United States Duration: Oct 11 1999 → Oct 14 1999

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1713
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	5th International Conference on Principles and Practice of Constraint Programming, CP 1999
Country/Territory	United States
City	Alexandria
Period	10/11/99 → 10/14/99

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
Computer Science(all)

Access to Document

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

Cite this

Suyama, T., Yokoo, M., & Nagoya, A. (1999). Solving satisfiability problems on FPGAs using experimental unit propagation. In J. Jaffar (Ed.), 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); Vol. 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. ed. / 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); Vol. 1713).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Suyama, T, Yokoo, M & Nagoya, A 1999, Solving satisfiability problems on FPGAs using experimental unit propagation. in J Jaffar (ed.), 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), vol. 1713, Springer Verlag, pp. 434-445, 5th International Conference on Principles and Practice of Constraint Programming, CP 1999, Alexandria, United States, 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. In Jaffar J, editor, 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)). doi: 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. editor / 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",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1999.; 5th International Conference on Principles and Practice of Constraint Programming, CP 1999 ; Conference date: 11-10-1999 Through 14-10-1999",

year = "1999",

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

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1999.

PY - 1999

Y1 - 1999

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

AN - SCOPUS:84957367729

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

T2 - 5th International Conference on Principles and Practice of Constraint Programming, CP 1999

Y2 - 11 October 1999 through 14 October 1999

ER -

Solving satisfiability problems on FPGAs using experimental unit propagation

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this