gnome
- 1,031
- 1
How would you describe this set in plain English:
[tex]\text{POS}_\lambda(\alpha) = \alpha_\lambda^0 \cup \{\kappa - \{\lambda\}|\kappa \in \alpha_\lambda^+\}[/tex]
where:
[itex]\lambda[/itex] is a literal
[itex]\kappa[/itex] is an [itex]\vee[/itex] clause with the set [itex]\kappa = \vee_{j\leq m}\;\lambda_j[/itex] represented as [itex]\kappa = \{\lambda_j|j \leq m \}[/itex]
[itex]\{\lambda\}[/itex] is a unit clause consisting of just a single literal [itex]\lambda[/itex]
a CNF formula [itex]\alpha[/itex] is a set [itex]\alpha = \wedge_{i\leq n}\;\kappa_i[/itex] represented as [itex]\alpha = \{\kappa_i|i \leq n \}[/itex]
a clause [itex]\kappa[/itex] is called [itex]\lambda-positive[/itex] if [itex]\lambda \in \kappa[/itex]
a clause [itex]\kappa[/itex] is called [itex]\lambda-negative[/itex] if [itex]\neg \lambda \in \kappa[/itex]
a clause [itex]\kappa[/itex] is called [itex]\lambda-neutral[/itex] if [itex]\kappa[/itex] is neither [itex]\lambda-positive[/itex] nor [itex]\lambda-negative[/itex]
if [itex]\alpha[/itex] is a set of clauses, [itex]\alpha_\lambda^+[/itex] is the set of [itex]\lambda-positive[/itex] clauses of [itex]\alpha[/itex], [itex]\alpha_\lambda^-[/itex] is the set of [itex]\lambda-negative[/itex] clauses of [itex]\alpha[/itex], and [itex]\alpha_\lambda^0[/itex] is the set of [itex]\lambda-neutral[/itex] clauses of [itex]\alpha[/itex].
At first, I was reading [itex]\text{POS}_\lambda(\alpha)[/itex] as the union of the [itex]\lambda-neutral[/itex] clauses of [itex]\alpha[/itex] with the [itex]\lambda-positive[/itex] clauses of [itex]\alpha[/itex] but excluding the unit clause [itex]\{\lambda\}[/itex]. But apparently it is intended to be read as the union of the [itex]\lambda-neutral[/itex] clauses of [itex]\alpha[/itex] with the [itex]\lambda-positive[/itex] clauses of [itex]\alpha[/itex] but with ALL of the [itex]\lambda[/itex] terms EXCLUDED from those clauses.
WHY is it read that way? Or, to put it another way, why was it not written as [itex]\text{POS}_\lambda(\alpha) = \alpha_\lambda^0 \cup \{\kappa - \lambda|\kappa \in \alpha_\lambda^+\}[/itex]. (Why did they put their [itex]\lambda[/itex] in brackets {}?) And how would you write set-builder notation for "the [itex]\lambda-positive[/itex] clauses of [itex]\alpha[/itex] but excluding just the unit clause [itex]\{\lambda\}[/itex]."
This comes from Computability, Complexity and Languages by Davis, Sigal and Weyuker, section 12.4, discussion of the Davis-Putnam rules for algorithms to manipulate CNF formulas.
[tex]\text{POS}_\lambda(\alpha) = \alpha_\lambda^0 \cup \{\kappa - \{\lambda\}|\kappa \in \alpha_\lambda^+\}[/tex]
where:
[itex]\lambda[/itex] is a literal
[itex]\kappa[/itex] is an [itex]\vee[/itex] clause with the set [itex]\kappa = \vee_{j\leq m}\;\lambda_j[/itex] represented as [itex]\kappa = \{\lambda_j|j \leq m \}[/itex]
[itex]\{\lambda\}[/itex] is a unit clause consisting of just a single literal [itex]\lambda[/itex]
a CNF formula [itex]\alpha[/itex] is a set [itex]\alpha = \wedge_{i\leq n}\;\kappa_i[/itex] represented as [itex]\alpha = \{\kappa_i|i \leq n \}[/itex]
a clause [itex]\kappa[/itex] is called [itex]\lambda-positive[/itex] if [itex]\lambda \in \kappa[/itex]
a clause [itex]\kappa[/itex] is called [itex]\lambda-negative[/itex] if [itex]\neg \lambda \in \kappa[/itex]
a clause [itex]\kappa[/itex] is called [itex]\lambda-neutral[/itex] if [itex]\kappa[/itex] is neither [itex]\lambda-positive[/itex] nor [itex]\lambda-negative[/itex]
if [itex]\alpha[/itex] is a set of clauses, [itex]\alpha_\lambda^+[/itex] is the set of [itex]\lambda-positive[/itex] clauses of [itex]\alpha[/itex], [itex]\alpha_\lambda^-[/itex] is the set of [itex]\lambda-negative[/itex] clauses of [itex]\alpha[/itex], and [itex]\alpha_\lambda^0[/itex] is the set of [itex]\lambda-neutral[/itex] clauses of [itex]\alpha[/itex].
At first, I was reading [itex]\text{POS}_\lambda(\alpha)[/itex] as the union of the [itex]\lambda-neutral[/itex] clauses of [itex]\alpha[/itex] with the [itex]\lambda-positive[/itex] clauses of [itex]\alpha[/itex] but excluding the unit clause [itex]\{\lambda\}[/itex]. But apparently it is intended to be read as the union of the [itex]\lambda-neutral[/itex] clauses of [itex]\alpha[/itex] with the [itex]\lambda-positive[/itex] clauses of [itex]\alpha[/itex] but with ALL of the [itex]\lambda[/itex] terms EXCLUDED from those clauses.
WHY is it read that way? Or, to put it another way, why was it not written as [itex]\text{POS}_\lambda(\alpha) = \alpha_\lambda^0 \cup \{\kappa - \lambda|\kappa \in \alpha_\lambda^+\}[/itex]. (Why did they put their [itex]\lambda[/itex] in brackets {}?) And how would you write set-builder notation for "the [itex]\lambda-positive[/itex] clauses of [itex]\alpha[/itex] but excluding just the unit clause [itex]\{\lambda\}[/itex]."
This comes from Computability, Complexity and Languages by Davis, Sigal and Weyuker, section 12.4, discussion of the Davis-Putnam rules for algorithms to manipulate CNF formulas.