Chaff es un algoritmo para resolver instancias del problema de satisfacibilidad booleano en programación. Fue diseñado por investigadores de la Universidad de Princeton , Estados Unidos. El algoritmo es una instancia del algoritmo DPLL con una serie de mejoras para una implementación eficiente.
Implementaciones
Algunas implementaciones disponibles del algoritmo en software son mChaff y zChaff , siendo esta última la más conocida y utilizada. zChaff fue escrito originalmente por el Dr. Lintao Zhang, ahora [ aclarar ] en Microsoft Research , de ahí la "z". Ahora lo mantienen investigadores de la Universidad de Princeton y está disponible para su descarga como código fuente y binarios en Linux . zChaff es gratuito para uso no comercial.
Referencias
- 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). "Solucionadores de satisfacción booleana y sus aplicaciones en la comprobación de modelos". Actas del IEEE . 103 (11). doi : 10.1109 / JPROC.2015.2455034 .