3
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

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.

Improve this answer
$\endgroup$
9
  • $\begingroup$ 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! $\endgroup$
    – Curious
    Jul 4, 2014 at 12:14
  • $\begingroup$ 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" $\endgroup$
    – Curious
    Jul 4, 2014 at 15:48
  • $\begingroup$ 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. $\endgroup$
    – Kyle Jones
    Jul 4, 2014 at 16:47
  • $\begingroup$ 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? $\endgroup$
    – Curious
    Jul 6, 2014 at 17:34
  • $\begingroup$ 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. $\endgroup$
    – Kyle Jones
    Jul 6, 2014 at 17:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.