|
Notas:
|
En este artículo se presenta una introducción a los algoritmos de satisfactibilidad.
Primero, se describe el procedimiento de Davis-Putnam, que constituye la base de la
mayoría de algoritmos completos (por ejemplo: Satz, SATO, GRASP y Chaff). Después,se presentan las mejoras que pueden incorporarse al procedimiento de Davis-Putnam para obtener un algoritmo competitivo: estructuras de datos optimizadas, heurísticas de selecciónn de variable, backtracking no cronológico, aprendizaje de cláusulas, aleatorización y reinicios. Finalmente, se describen GSAT y WalkSAT, que son los algoritmos incompletos de búsqueda local más utilizados. |
