Agnar algoritm
Chaff är en algoritm för att lösa instanser av det booleska tillfredsställelseproblemet i programmering. Den designades av forskare vid Princeton University . Algoritmen är en instans av DPLL-algoritmen med ett antal förbättringar för effektiv implementering.
Genomföranden
Några tillgängliga implementeringar av algoritmen i mjukvara är mChaff och zChaff , den senare är den mest kända och använda. zChaff skrevs ursprungligen av Dr. Lintao Zhang, nu [ förtydliga ] på Microsoft Research , därav "z". Den underhålls nu av forskare vid Princeton University och är tillgänglig för nedladdning som både källkod och binärfiler på Linux . zChaff är gratis för icke-kommersiellt bruk.
- M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik. Chaff: Engineering an Efficient SAT Solver , 39th Design Automation Conference (DAC 2001), Las Vegas, ACM 2001.
- Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Booleska tillfredsställelselösare och deras tillämpningar i modellkontroll". IEEE:s förfaranden . 103 (11). doi : 10.1109/JPROC.2015.2455034 .
externa länkar