Spreu-Algorithmus - Chaff algorithm

Chaff ist ein Algorithmus zum Lösen von Instanzen des Booleschen Erfüllbarkeitsproblems in der Programmierung. Es wurde von Forschern der Princeton University in den USA entwickelt. Der Algorithmus ist eine Instanz des DPLL-Algorithmus mit einer Reihe von Verbesserungen für eine effiziente Implementierung.

Implementierungen

Einige verfügbare Implementierungen des Algorithmus in Software sind mChaff und zChaff , wobei letztere die bekannteste und am weitesten verbreitete ist. zChaff wurde ursprünglich von Dr. Lintao Zhang, jetzt bei Microsoft Research , geschrieben, daher das „z“. Es wird jetzt von Forschern der Princeton University gepflegt und steht sowohl als Quellcode als auch als Binärdateien unter Linux zum Download zur Verfügung . zChaff ist für die nicht-kommerzielle Nutzung kostenlos.

Verweise

  • M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik. Spreu: Engineering an Efficient SAT Solver , 39. Design Automation Conference (DAC 2001), Las Vegas, ACM 2001.
  • Vizel, Y.; Weißenbacher, G.; Malik, S. (2015). „Boolesche Erfüllbarkeitslöser und ihre Anwendungen in der Modellprüfung“. Verfahren der IEEE . 103 (11). doi : 10.1109/JPROC.2015.2455034 .

Externe Links


Stub-Symbol

Dieser Artikel zu formalen Methoden ist ein Stummel . Sie können Wikipedia helfen, indem Sie es erweitern .