UNSAT — Jemoka Knowledge Base

\begin{equation} \text{UNSAT} = \left\{\phi : \text{all assignment make $\phi$ false}\right\} \end{equation}

Equivalently, we have:

\begin{equation} \text{UNSAT} = \neg \text{SAT} \end{equation}

NP = coNP IFF UNSAT is in NP \begin{equation} \text{NP} = \text{coNP} \Leftrightarrow \text{UNSAT} \in \text{NP} \end{equation} \Rightarrow Because \text{UNSAT} \in \text{coNP}, and we hypothesize NP = coNP, so \text{UNSAT} \in \text{NP} \Leftarrow Suppose UNSAT in NP, we desire that \text{coNP} = NP. Let L \in \text{coNP},so \neg L \in \text{NP}, since SAT is NP-complete, we can write that L \leq_{p} \text{SAT}. Equivalently, we have L \leq_{p} \neg \text{SAT} = \text{UNSAT}. Since \text{UNSAT} \in \text{coNP}, we have L \in \text{NP}. In particular this proves that UNSAT is coNP-complete coNP complete L is coNP complete if L \in \text{coNP} \forall A \in \text{coNP}, A \leq_{p} L key detail: L is NP complete IFF \neg L is coNP complete. Corollary: L is NP-Complete IFF \neg L is NP-Complete.