Satisfiability equivalence

Satisfiability equivalence is a property that can apply between two predicate logic formulas.

Two formulas F and G are equivalent to satisfiability if and only if:

F is satisfiable G is satisfiable ${\displaystyle \Leftrightarrow }$

Or the other way around:

F is unsatisfiable G is unsatisfiable ${\displaystyle \Leftrightarrow }$

The two formulas do not need to be equivalent and do not need to be satisfied by the same interpretations . Satisfiability equivalence is therefore a rather weak property.

The satisfiability equivalence is relevant when demonstrating the unsatisfiability of a predicate logic formula using the Herbrand theory . To do this, the formula must first be converted into the Skolem form , which is merely equivalent to the original formula.

example

Let it be a formula (with the condition that it is neither a tautology nor unsatisfiable). Then the formulas and are equivalent, but not equivalent. ${\displaystyle X}$ ${\displaystyle X}$ ${\displaystyle \neg X}$

Transformation into satisfiability-equivalent 3-KNF formula

For every formula in m- CNF , i. H. the form with at most literals per disjunction, a satisfiability-equivalent formula in 3-CNF can be constructed in polynomial time. ${\displaystyle \bigwedge _{i}\left(Y_{i,1}\vee ...\vee Y_{i,k_{i}}\right)}$ ${\displaystyle k_{i}\leq m}$ ${\displaystyle m}$

Be with it . As long as even one clause has this replaced by with ${\displaystyle \Psi =C_{1}\wedge ...\wedge C_{n}}$ ${\displaystyle C_{i}=Y_{i,1}\vee ...\vee Y_{i,m_{i}}}$ ${\displaystyle \Psi }$ ${\displaystyle m_{i}\geq 3}$ ${\displaystyle C_{i}}$ ${\displaystyle C_{i}=C'_{i}\wedge C''_{i}}$

${\displaystyle C'_{i}=Y_{i,1}\vee Y_{i,2}\vee X}$

${\displaystyle C''_{i}=\neg X\vee Y_{i,3}\vee ...\vee Y_{i,m_{i}}}$

${\displaystyle X}$is a new variable. Any interpretation that and met also met . Any interpretation that satisfies can be transformed into an interpretation that satisfies and . ${\displaystyle C'_{i}}$ ${\displaystyle C''_{i}}$ ${\displaystyle C_{i}}$ ${\displaystyle C_{i}}$ ${\displaystyle C'_{i}}$ ${\displaystyle C''_{i}}$