Algoritmo de chaff

Chaff es un algoritmo para resolver instancias del problema de satisfacibilidad booleana en programación. Fue diseñado por investigadores de la Universidad de Princeton . El algoritmo es una variante del algoritmo DPLL con varias mejoras para una implementación eficiente.

Algunas implementaciones disponibles del algoritmo en software son mChaffy zChaff, siendo esta última la más conocida y utilizada. zChaff fue escrito originalmente por el Dr. Lintao Zhang, de ahí la “z”. Actualmente, investigadores de la Universidad de Princeton lo mantienen y está disponible para su descarga como código fuente y binarios en Linux . zChaff es gratuito para uso no comercial.

• M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik. Chaff: Ingeniería de un solucionador SAT eficiente , 39.ª Conferencia de Automatización del Diseño (DAC 2001), Las Vegas, ACM 2001.
• Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Solucionadores de satisfacibilidad booleana y sus aplicaciones en la verificación de modelos". Actas del IEEE . 103 (11): 2021– 2035. doi : 10.1109/JPROC.2015.2455034 . S2CID 10190144 . 

• Página web sobre zChaff