Saber si una fórmula (µ) es satisfacible o no

Saber si una fórmula (µ) es satisfacible o no

1. Tabla de verdad

   • El número de la tabla crece exponencialmente según el numero de variables.
   • 1.Según el número de variables, se enlistan todas las combinaciones posibles de valores de verdad.
     • 2.Dichas combinaciones se evalúan en la fórmula.
       • 3.Cada fila de la tabla escupe que valor de verdad que toma la fórmula según el estado de las variables.
         • Sí todas las casillas que correspondientes a la formula están evaluadas a verdadero.
           • Si todas se evalúan a falso.
             • Otro caso.
               • Es satisfacible, pues sabemos que existe aunque sea un modelo.
             • Es contradicción y no es satisfacible.
           • Es una tautología y la fórmula es satisfacible.

2. Tableau

   • Negamos la fórmula
     • Eliminamos equivalencias e implicaciones
   • Se construye en forma de árbol.
   • Si tenemos una conjunción el árbol crece 2 ramas hacia abajo.
   • Si tenemos una disyunción se desglosa en 2 ramas.
   • Buscamos cerrar ramas encontrando contradicciones.
   • Si logramos cerrar todas las ramas o algunas, µ es satisfacible.
   • En otro caso no lo es.

3. Resolución binaria

   • Se lleva a µ a su forma normal conjuntiva
     • Una vez hecho esto se enlistan las cláusulas
       • Y usando la reducción Binaria de Robinson se busca llegar a tener una literal y su complemento.
         • Si esto ocurre, la cláusula vacía nos dice que µ es insatisfacible.
           • Si no se puede llegar a la cláusula vacía µ es satisfacible.
             • Puede usarse refutación

4. Interpretaciones

   • Se propone que el valor de verdad de la fórmula es verdadero.
   • Se busca encontrar una combinación de valores de verdad en las variables.
   • Tal que dicha combinación sea un modelo en µ
   • Si es posible dar con el modelo, entonces µ es satisfacible, en otro caso es una contradicción.

5. Equivalencias

   • Dadas ciertas reglas descomponemos una formula a expresiones más sencillas
   • buscamos hacer la fórmula lo mas pequeña posible
   • logrado eso, si tenemos T ó una fórmula es satisfacible
   • Si llegamos a una contradicción no es satisfacible.