# 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?

## 1 Answer

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.

• Thank you for the reply. I am glad that you always come to my rescue!. Doubt: I didn't get the last line, i.e., 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. I would be grateful if you could explain this with the help of an example. Secondly, what are the cases when we cannot ignore the quantifiers? Thanks! – Curious Jul 4 '14 at 12:14
• Also, converting a quantified horn formula into an equivalent propositional horn formula results in exponentially longer formula. ub-net.de/cms/fileadmin/upb/doc/bubeck-qhorn-dam-2008.pdf on Page 5 under the heading "Eliminating universal Quantifiers" – Curious Jul 4 '14 at 15:48
• But we're not talking about converting a quantified formula into an equivalent unquantified one. For the sake of the test only strip off the quantifiers; they don't matter. Only the satisfiability of the constructed stripped 2-SAT formula matters. – Kyle Jones Jul 4 '14 at 16:47
• Will the Horn renamability test that we are applying also give the renaming set, i.e. the variables which we have to rename in order to get the quantified horn formula? – Curious Jul 6 '14 at 17:34
• Yes. After you find a solution to the 2-SAT test formula, the variables whose values are true in the solution are the ones to polarity flip in the original formula to produce a Horn formula. – Kyle Jones Jul 6 '14 at 17:55