Accelerating boolean satisfiability through application specific processing

ABSTRACT

This paper presents our work in developing an application specific multiprocessor system for SAT, utilizing the most recent results such as the development of highly efficient sequential SAT algorithms, the emergence of commercial configurable processor cores and the rapid progress in IC manufacturing techniques. Based on an analysis of the basic SAT search algorithm, we propose a new parallel SAT algorithm that utilizes fine grain parallelism. This is then used to design a multiprocessor architecture in which each processing node consists of a processor and a communication assist node that deals with message processing. Each processor is an application specific processor built from a commercial configurable processor core. All the system configurations are determined based on the characteristics of SAT algorithms, and are supported by simulation results. While this hardware accelerator system does not change the inherent intractability of the SAT problems, it achieves a 30-60x speedup over and above the fastest known SAT solver - Chaff. We believe that this system can be used to expand the practical applicability of SAT in all its application areas.

REFERENCES

• 1: P. Stephan, R. Brayton, and A. Sangiovanni-Vincentelli. Combinational Test Generation Using Satisfiability. In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, pages 1167-1176, September 1996.
• 2: W. Kunz and D. Sotoffel. Reasoning in Boolean Networks. Kluwer Academic Publishers, 1997.
• 3: S. Devadas. Optimal Layout via Boolean Satisfiability. In Proceedings of IEEE International Conference on Computer-Aided Design, 1989.
• 4: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 5: João P. Marques Silva , Karem A. Sakallah, GRASP—a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.220-227, November 10-14, 1996, San Jose, California, United States
• 6: Hantao Zhang, SATO: An Efficient Propositional Prover, Proceedings of the 14th International Conference on Automated Deduction, p.272-275, July 13-17, 1997
• 7: C min Li. Equivalency Reasoning to solve a class of hard SAT problems. Available from http://www.cs.washington.edu/homes/kautz/challenge/cli.ps.
• 8: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 9: Miron Abramovici , Daniel G. Saab, Satisfiability on reconfigurable hardware, Proceedings of the 7th International Workshop on Field-Programmable Logic and Applications, p.448-456, September 01-03, 1997
• 10: Peixin Zhong , Margaret Martonosi , Pranav Ashar , Sharad Malik, Solving Boolean Satisfiability with Dynamic Hardware Configurations, Proceedings of the 8th International Workshop on Field-Programmable Logic and Applications, From FPGAs to Computing Paradigm, p.326-335, August 31-September 03, 1998
• 11: Xtensa configurable processor. http://www.tensilica.com
• 12: Benjamin W. Wah, Guo-Jie Li and Chee Fen Yu. Multiprocessing of combinational search problems. In IEEE computer. Pages 93-108, June 1985.
• 13: Curt Powley , Chris Ferguson , Richard E. Korf, Parallel heuristic search: two approaches, Parallel algorithms for machine intelligence and vision, Springer-Verlag New York, Inc., New York, NY, 1990
• 14: Y. Zhao, S. Malik, M. Moskewicz and C.Madigan. Matching Architecture to Application via Configurable Processors: A Case Study with Boolean Satisfiability. In Proceedings of International Conference on Computer Design, 2001.
• 15: Velev, M., FVP-UNSAT.1.0, FVP-UNSAT.2.0, VLIW-SAT. 1.0, SSS-SAT.1.0, Superscalar Suite 1.0/1.0a, Available from: http://www.ece.cmu.edu/~mvelev.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.0 GENERAL
      Subjects: Modeling of computer architecture

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.1 Types and Design Styles
          Subjects: Microprocessors and microcomputers

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Parallelism and concurrency

General Terms:
Design, Experimentation, Performance

Keywords:
application specific, boolean satisfiability, configurable processor core, multiprocessor