Advertisement

One Flip per Clock Cycle

  • Martin Henz
  • Edgar Tan
  • Roland Yap
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2239)

Abstract

Stochastic Local Search (SLS) methods have proven to be successful for solving propositional satisfiability problems (SAT). In this paper, we show a hardware implementation of the greedy local search procedure GSAT. With the use of field programmable gate arrays (FPGAs), our implementation achieves one flip per clock cycle by exploiting maximal parallelism and at the same time avoiding excessive hardware cost. Experimental evaluation of our prototype design shows a speedup of two orders of magnitude over optimized software implementations and at least one order of magnitude over existing hardware schemes. As far as we are aware, this is the fastest known implementation of GSAT. We also introduce a high level algorithmic notation which is convenient for describing the implementation of such algorithms in hardware, as well as an appropriate performance measure for SLS implementations in hardware.

Keywords

Clock Cycle Field Programmable Gate Array Satisfying Assignment FPGA Implementation Gate Delay 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Ad00]
    Miron Abramovici and Jose T. de Sousa. A SAT solver using reconfigurable hardware and virtual logic. Journal of Automated Reasoning, 24(1–2):37–65, February 2000.MathSciNetGoogle Scholar
  2. [APR+96]
    M. Aubury, I. Page, G. Randall, J. Saul, and R. Watts. Handel-C language reference guide. Technical report, Oxford University Computing Laboratory, Oxford, UK, 1996.Google Scholar
  3. [BHSZ95]
    Guy Blelloch, Jonathan Hardwick, Jay Sipelstein, and Marco Zagha. NESL user’s manual, version 3.1. Technical Report CMU-CS-95-169, Carnegie Mellon University, Pittsburgh, PA, 1995.Google Scholar
  4. [BM99]
    Guy Blelloch and Bruce Maggs. Parallel algorithms. In Algorithms and Theory of Computation Handbook. CRC Press, Boca Raton, Florida, 1999.Google Scholar
  5. [DeH96]
    A. DeHon. Reconfigurable Architectures for General-Purpose Computing. PhD thesis, The MIT Press, Cambridge, MA, September 1996.Google Scholar
  6. [Gu92]
    J. Gu. Efficient local search for very large-scale satisifiability problems. SIGART Bulletin, (3):8–12, 1992.Google Scholar
  7. [HM97]
    Youssef Hamadi and David Merceron. Reconfigurable architectures: A new vision for optimization problems. In Gert Smolka, editor, Principles and Practice of Constraint Programming-CP97, Proceedings of the 3rd International Conference, Lecture Notes in Computer Science 1330, pages 209–221, Linz, Austria, 1997. Springer-Verlag, Berlin.Google Scholar
  8. [Hoo96]
    Holger Hoos. Aussagenlogische SAT-Verfahren und ihre Anwendung bei der Lösung des HC-Problems in gerichteten Graphen. Diplomarbeit. Fachbereich Informatik, Technische Hochschule Darmstadt, Germany, March 1996.Google Scholar
  9. [HS00]
    Holger H. Hoos and Thomas Stützle. Local search algorithms for SAT: An empirical evaluation. Journal of Automated Reasoning, 24(4):421–481, 2000.zbMATHCrossRefGoogle Scholar
  10. [MSK97]
    David McAllester, Bart Selman, and Henry Kautz. Evidence for invariants in local search. In Proceedings Fourteenth National Conference on Artificial Intelligence (AAAI-97), 1997.Google Scholar
  11. [Pag96]
    I. Page. Constructing hardware-software systems from a single description. Journal of VLSI Signal Processing, (12):87–107, 1996.CrossRefMathSciNetGoogle Scholar
  12. [SKC94]
    B. Selman, H. Kautz, and B. Cohen. Noise strategies for improving local search. In Proceedings of AAAI-94, pages 337–343, 1994.Google Scholar
  13. [SLM92]
    B. Selman, Hector Levesque, and David Mitchell. A new method for solving hard satisfiability problems. In Proceedings of AAAI-92, pages 440–446, 1992.Google Scholar
  14. [YSLL99]
    Wong Hiu Yung, Yuen Wing Seung, Kin Hong Lee, and Philip Heng Wai Leong. A runtime reconfigurable implementation of the GSAT algorithm. In Patrick Lysaght, James Irvine, and Reiner W. Hartenstein, editors, Field-Programmable Logic and Applications, pages 526–531. Springer-Verlag, Berlin, / 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Martin Henz
    • 1
  • Edgar Tan
    • 1
  • Roland Yap
    • 1
  1. 1.School of ComputingNational University of SingaporeSingapore

Personalised recommendations