Algorytm plew
Chaff to algorytm do rozwiązywania przypadków problemu spełnialności Boole'a w programowaniu. Został zaprojektowany przez naukowców z Princeton University . Algorytm jest instancją algorytmu DPLL z szeregiem ulepszeń zapewniających wydajną implementację.
Implementacje
Niektóre dostępne implementacje algorytmu w oprogramowaniu to mChaff i zChaff , przy czym ta ostatnia jest najbardziej znana i używana. zChaff został pierwotnie napisany przez dr Lintao Zhanga, obecnie [ wyjaśnij ] w Microsoft Research , stąd „z”. Obecnie jest utrzymywany przez naukowców z Princeton University i dostępny do pobrania zarówno jako kod źródłowy, jak i pliki binarne w systemie Linux . zChaff jest darmowy do użytku niekomercyjnego.
- 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.
- Wizel, Y.; Weissenbacher, G.; Malik, S. (2015). „Rozwiązania spełnialności boolowskiej i ich zastosowania w sprawdzaniu modeli”. Obrady IEEE . 103 (11). doi : 10.1109/JPROC.2015.2455034 .
Linki zewnętrzne