Efficient distributed SAT and SAT-based distributed bounded model checking

Malay K. Ganai, Aarti Gupta, Zijiang Yang, Pranav Ashar

Research output: Chapter in Book/Report/Conference proceedingChapter

8 Scopus citations

Abstract

SAT-based Bounded Model Checking (BMC), though a robust and scalable verification approach, still is computationally intensive, requiring large memory and time. Interestingly, with the recent development of improved SAT solvers, it is frequently the memory limitation of a single server rather than time that becomes a bottleneck for doing deeper BMC search. Distributing computing requirements of BMC over a network of workstations can overcome the memory limitation of a single server, albeit at increased communication cost. In this paper, we present: a) a method for distributed-SAT over a network of workstations using a Master/Client model where each Client worsktation has an exclusive partition of the SAT problem and uses knowledge of partition topology to communicate with other Clients, b) a method for distributing SAT-based BMC using the distributed-SAT. For the sake of scalability, at no point in the BMC computation does a single workstation have all the information. We experimented on a network of heterogenous workstations interconnected with a standard Ethernet LAN. To illustrate, on an industrial design with -13K FFs and -0.5M gates, the non-disributed BMC on a single workstation (with 4 Gb memory) ran out of memroy after reaching a depth of 120; on the otherhand, our SAT-based distributed BMC over 5 similar workstations was able to go upto 323 steps with a communication overhead of only 30%.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsDaniel Geist, Enrico Tronci
PublisherSpringer Verlag
Pages334-347
Number of pages14
ISBN (Print)354020363X
DOIs
StatePublished - 2003
Externally publishedYes

Publication series

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

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Efficient distributed SAT and SAT-based distributed bounded model checking'. Together they form a unique fingerprint.

  • Cite this

    Ganai, M. K., Gupta, A., Yang, Z., & Ashar, P. (2003). Efficient distributed SAT and SAT-based distributed bounded model checking. In D. Geist, & E. Tronci (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 334-347). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2860). Springer Verlag. https://doi.org/10.1007/978-3-540-39724-3_30