patternMinor
Can quantified renamable Horn formulas be identified using the same procedure as unquantified formulas?
Viewed 0 times
unquantifiedcanthesameformulasprocedurehornrenamableusingquantified
Problem
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?
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?
Solution
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.
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.
Context
StackExchange Computer Science Q#28058, answer score: 4
Revisions (0)
No revisions yet.