SAT (satisfacilidad)
Problema de satisfacibilidad booleana
Resolvedores
Tablas de verdad.
Este es el metodo más obvio para ver si existe un modelo para una formula.
Como el conjunto de variables es finito, tambien vemos que el número de posibles asignación es finito,en concreto dos elevado al número de variables que tengamos
El método de tableros de verdad va probando uno a uno cada
posible modelo comprobando en cada caso si hace cierta la fórmula. En caso
de encontrar alguno sabemos que la fórmula es satisfactible, en caso
contrario sabemos que es insatisfaccible
Tablero semantico
El método de tableros semánticos organiza de manera sistemática la
búsqueda de modelos, reduciendo la satisfactiblidad de las fórmulas
consideradas a la de ciertos conjuntos de literales
Algoritmo dos fases
Este algoritmo utiliza dos etapas bien diferenciadas, por un lado se parte de
una solución inicial (que no tiene porque ser correcta) proporcionada por una
heurística (GSAT). En la segunda fase se mejora esa solución hasta terminar
el algoritmo.
