Advertisement

Ein paralleler SAT-Solver auf Transputern

  • Max Böhm
  • Ewald Speckenmeyer
Conference paper
Part of the Informatik aktuell book series (INFORMAT)

Zusammenfassung

Wir beschreiben ein schnelles paralleles Programm zur Lösung des NP—vollständigen Erfüllbarkeitsproblems (SAT). Das Programm ist eine Paiallelisierung des zur Zeit schnellsten sequentiellen SAT—Solvers, dem Siegerprogramm des Padorboruer SAT—Wettbewerbs 1992. Neben dem sequentiellen Algorithmus, der als Rechenprozeß auf jedem Transputer läuft, beschreiben wir ein effizientes Verfahren zum Lastausgleich über die Hypercube—Vernetzung. Wir geben Testergebnisse für Random 3—SAT Formeln mit bis zu 400 Variablen aus dem ‘schweren’ Bereich (1600 bis 2000 Klauseln) bei bis zu 128 Prozessoren an. Bei unerfüllbaren Formeln wurde ein nahezu linearer Speedup erzielt, der bei erfüllbaren Formeln im Mittel deutlich übertroffen wurde, siehe [2].

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Literatur

  1. 1.
    Davis, M. and Putnam, H.: A computing procedure for quantification theory, J. ACM 8, 1960, 201–215MathSciNetCrossRefGoogle Scholar
  2. 1.
    Speckenmeyer, E.: Is average superlinear speedup possible?, Proc. CSL’88, Springer-Verlag (LNCS 385), 1989, 301–312Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Max Böhm
    • 1
  • Ewald Speckenmeyer
    • 1
  1. 1.Düsseldorf Mathematisches Institut/Abteilung für InformatikHeinrich—Heine—UniversitätDüsseldorf 1Deutschland

Personalised recommendations