Advertisement

Run-Time Performance Optimization of an FPGA-Based Deduction Engine for SAT Solvers

  • Andreas Dandalis
  • Viktor K. Prasanna
  • Bharani Thiruvengadam
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2147)

Abstract

FPGAs are a promising technology for accelerating SAT solvers. Besides their high density, fine granularity, and massive parallelism, FPGAs provide the opportunity for run-time customization of the hardware based on the given SAT instance. In this paper, a parallel deduction engine is proposed for backtrack search algorithms. The performance of the deduction engine is critical to the overall performance of the algorithm since, for any moderate SAT instance, millions of implications are derived. We propose a novel approach in which, p, the amount of parallelization of the engine is fine-tuned during problem solving in order to optimize performance. Not only the hardware is initially customized based on the input instance, but it is also dynamically modified in terms of p based on the knowledge gained during solving the SAT instance. Compared with conventional deduction engines that correspond to p = 1, we demonstrate speedups in the range of 2.87 - 5.44 for several SAT instances.

Keywords

Clock Cycle Clock Speed Input Instance Conjunctive Normal Form Formula Baseline Solution 
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. 1.
    M. Abramovici and D. Saab, “Satisfiability on Reconfigurable Hardware,” International Conference on Field Programmable Logic and Applications, September 1997.Google Scholar
  2. 2.
    M. Abramovici, J. Sousa, and D. Saab,“A Massively-Parallel Easily-Scalable Satisfiability Solver using Reconfigurable Hardware,” ACM/IEEE Design Automation Conference, 1999.Google Scholar
  3. 3.
    T. H. Cormen, C. E. Leiserson, and R. L. Rivest, “Introduction to Algorithms,” The MIT Press, Cambridge Massachusetts, 1997.Google Scholar
  4. 4.
    A. Dandalis, “Dynamic Logic Synthesis for Reconfigurable Devices,” PhD Thesis, Dept. of Electrical Engineering, University of Southern California. Under Preparation.Google Scholar
  5. 5.
    M. Davis and H. Putnam, “A Computing Procedure for Quantification Theory,” Journal of ACM, 7:201–215, 1960.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
  7. 7.
    M. Platzner and G. De Micheli, “Acceleration of Satisfiability Algorithms by Reconfigurable Hardware,” International Conference on Field Programmable Logic and Applications, September 1998.Google Scholar
  8. 8.
    M. Redekopp and A. Dandalis, “A Parallel Pipelined SAT Solver for FPGAs,” International Conference on Field Programmable Logic and Applications, September 2000.Google Scholar
  9. 9.
    J. P. M. Silva, “An Overview of Backtrack Search Satisfiability Algorithms,” International Symposium on Artificial Intelligence and Mathematics, January 1998.Google Scholar
  10. 10.
    J. P. M. Silva and K. A. Sakallah, “GRASP: A New Search Algorithm for Satisfiability,”CSE-TR-292-96, Computer Science and Engineering Department, University of Michigan, Ann Arbor, April 1996.Google Scholar
  11. 11.
    T. Suyama, M. Yokoo, and H. Sawada, “Solving Satisfiability Problems on FPGAs,” International Conference on Field Programmable Logic and Applications, September 1996.Google Scholar
  12. 12.
    Xilinx Inc., http://www.xilinx.com
  13. 13.
    H. Zhang and M. Stickel, “An Efficient Algorithm for Unit-Propagation,” International Symposium on Artificial Intelligence and Mathematics, 1996.Google Scholar
  14. 14.
    P. Zhong, M. Martonosi, P. Ashar, and S. Malik, “Accelerating Boolean Satisfiability with Configurable Hardware,” IEEE Symposium on FPGAs for Custom Computing Machines, April 1998.Google Scholar
  15. 15.
    P. Zhong, M. Martonosi, S. Malik, and P. Ashar, “Solving Boolean Satisfiability with Dynamic Hardware Configurations,” International Workshop on Field Programmable Logic and Applications, September 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Andreas Dandalis
    • 1
  • Viktor K. Prasanna
    • 1
  • Bharani Thiruvengadam
    • 1
  1. 1.University of Southern CaliforniaLos AngelesUSA

Personalised recommendations