# Can quantified renamable Horn formulas be identified using the same procedure as unquantified formulas?

Definition: A renamable Horn formula is a Boolean formula that can be transformed into a Horn formula by flipping the polarity of every instance of one of more of its variables.

Example:

$\qquad (x_1 \lor x_2 \lor x_3)\land (\lnot x_1 \lor \lnot x_2 \lor x_3)$

This formula is renamable Horn because flipping the polarity of $x_2$ and $x_3$ produces the Horn formula

$\qquad (x_1 \lor \lnot x_2 \lor \lnot x_3)\land (\lnot x_1 \lor x_2 \lor \lnot x_3)$

Can I extend the test procedure for identifying renamable Horn formulas, as described in the Harry Lewis paper "Renaming a Set of Clauses as a Horn Set", to quantified formulas?

The paper states: Let $S$ be a set of clauses, say $S = (C_1 ..... C_m)$, where each $C_i = (L_{i1} .... , L_{il})$. Then define $S^*$ to be the set of clauses

$\qquad \bigcup_{i=1}^m \bigcup_{1\leq j <k\leq l} ((L_{ij}, L_{ik}))$.

Then $S$ is renamable-Horn if and only if $S^*$ is satisfiable.

Is this procedure applicable to quantified Boolean formulas also?

For unquantified formulas renaming a variable leaves satisfiability unchanged because a solution to the renamed formula is the same as a solution to the original formula except that the renamed variable has its value negated in compensation for the polarity change. The same is true for existentially quantified variables in a quantified formula, and for the same reason. For universally quantified variables, observe that the universal quantifier already requires satisfiability to survive a polarity flip because any solution has to encompass both true and false values for any universally quantified variable. That is, $\forall x(x)$ and $\forall x(\lnot x)$ offer the same solution constraint; the clause must be satisfied with $x$ taking both the true and false values.