En lógica matemática (un subtema dentro del campo de la lógica formal ), dos fórmulas son equisatisfactibles si la primera fórmula lo es siempre que la segunda lo sea y viceversa; en otras palabras, ambas fórmulas son satisfactorias o no lo son. [1] Sin embargo, las fórmulas equisatisfacibles pueden no estar de acuerdo para una elección particular de variables. Como resultado, la equisatisfacibilidad es diferente de la equivalencia lógica , ya que dos fórmulas equivalentes siempre tienen los mismos modelos. Mientras que dentro de las fórmulas equisatisfacibles, sólo se valora la proposición primitiva que impone la fórmula.
La equisatisfabilidad se utiliza generalmente en el contexto de la traducción de fórmulas, de modo que se puede definir que una traducción es correcta si las fórmulas original y resultante son equisatisfacibles. Ejemplos de traducciones que preservan la equisatisfacibilidad son la eskolemización y algunas traducciones a la forma normal conjuntiva, como la transformación de Tseytin .
Una traducción de lógica proposicional a lógica proposicional en la que cada disyunción binaria se reemplaza por , donde hay una nueva variable (una para cada disyunción reemplazada) es una transformación en la que se preserva la satisfacibilidad: las fórmulas original y resultante son equisatisfactibles. Tenga en cuenta que estas dos fórmulas no son equivalentes: la primera fórmula tiene el modelo en el que es verdadero mientras que y son falsos (el valor de verdad del modelo por ser irrelevante para el valor de verdad de la fórmula), pero este no es un modelo de la segunda fórmula. , lo cual tiene que ser cierto en este caso.
