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 &lt;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?
Yes.  The quantifiers can be ignored for the sake of the test since a quantified Horn formula is syntactically identical to an unquantified one except for the quantifiers.  That is, a quantified Horn formula still consists of only of clauses with zero or one positive literals.  The test only determines whether any combination of polarity flips could produce a Horn formula.

In order for the test to be useful for quantified formulas, it only remains to show that a quantified formula can be renamed and remain equisatisfiable with the original formula.

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.