Self reducibility lemma

The self reducibility lemma explains how 1-assignments of a given propositional formula relate to 1-assignments obtained from the formula by "setting" a variable to true or false.

Self reducibility lemma Let $\varphi$ be a propositional formula, $V = \text{vars}(\varphi)$, $X_i \in V$, and $W = V \setminus \{X_i\}$. Consider the formulas $\varphi_0$ and $\varphi_1$ defined by \begin{align} \varphi_0 & = \varphi\{X_i \mapsto \bot\} \enspace,\\ \varphi_1 & = \varphi\{X_i \mapsto \top\} \enspace. \end{align}

1. The formula $\varphi$ is satisfiable if, and only if, at least one of $\varphi_0$ and $\varphi_1$ is satisfiable.
2. Let $\beta \colon V \to \{0,1\}$ be a 1-assignment for $\varphi$. Then $\beta \vert_{W}$ is a 1-assignment for $\varphi_{\beta(X_i)}$.
3. Let $\gamma \colon W \to \{0,1\}$ be a 1-assignment for $\varphi_b$ for some $b \in \{0,1\}$. Then $\gamma \cup \{X_i \mapsto b\}$ is a 1-assignment for $\varphi$.

Proof For the proof, first note that 1. follows from 2. and 3.

Let $\sigma_0 = \{X_i \mapsto \bot\}$ and $\sigma_1 = \{X_i \mapsto \top\}$.

To prove 2., let $\beta \colon V \to \{0,1\}$ be a 1-assignment for $\varphi$ and let $b = \beta(X_i)$. Let $\delta \colon \text{PVars} \to \{0, 1\}$ be any extension. Then $\delta^{\sigma_b} = \delta$. Therefore, \begin{align} \llbracket \varphi \rrbracket_\beta & = \llbracket \varphi \rrbracket_{\delta} && \text{coincidence lemma}\\ & = \llbracket \varphi \rrbracket_{\delta^{\sigma_b} } && \text{see above}\\ & = \llbracket \varphi\sigma_b \rrbracket_\delta && \text{substitution lemma}\\ & = \llbracket \varphi_b \rrbracket_\delta && \text{substitution lemma and definition of $\varphi_b$}\\ & = \llbracket \varphi_b \rrbracket_{\delta \vert_W} && \text{coincidence lemma}\\ & = \llbracket \varphi_b \rrbracket_{\beta \vert_W } && \text{definition of $\delta$.} \end{align} For the proof of 3., let $b \in \{0,1\}$ and $\gamma \colon W \to \{0,1\}$ a 1-assignment for $\varphi_b$. Let $\delta \colon \text{PVars} \to \{0, 1\}$ be any extension of $\gamma$ such that $\delta(X_i) = b$. Now note that $\delta^{\sigma_b} = \delta$. Therefore, \begin{align} \llbracket \varphi_b \rrbracket_\gamma & = \llbracket \varphi_b \rrbracket_\delta && \text{coincidence lemma}\\ & = \llbracket \varphi\sigma_b \rrbracket_\delta && \text{definition of $\varphi_b$}\\ & = \llbracket \varphi \rrbracket_{\delta^{\sigma_b} } && \text{substitution lemma}\\ & = \llbracket \varphi \rrbracket_{\delta } && \text{see above}\\ & = \llbracket \varphi \rrbracket_{\gamma \cup \{X_i \mapsto b\} } && \text{coincidence lemma.} \end{align} This concludes the proof of the lemma.

This lemma is (can be) used to justify the correctness of several SAT solvers: .