Tseitin extension variables for subformulas

Given a Boolean formula $\phi$, a Tseitin extension variable for a subformula $\theta$ of $\phi$ is a fresh variable $y_{\theta }$ intended to represent the truth value of $\theta$. The Tseitin translation adds a local constraint for every subformula. For an atomic variable or constant it forces $y_{\theta }\leftrightarrow \theta$ directly; for a composite subformula it forces $y_{\theta }$ to equal the result of applying the outer connective to the extension variables of the immediate subformulas. It then requires the root variable $y_{\phi }$ to be true.

• The new variables name intermediate subformulas instead of expanding them repeatedly.

• This keeps the transformed formula linear in the size of the original parse tree.