- #1
gnome
- 1,031
- 1
How would you describe this set in plain English:
\text{POS}_\lambda(\alpha) = \alpha_\lambda^0 \cup \{\kappa - \{\lambda\}|\kappa \in \alpha_\lambda^+\}
where:
\lambda is a literal
\kappa is an \vee clause with the set \kappa = \vee_{j\leq m}\;\lambda_j represented as \kappa = \{\lambda_j|j \leq m \}
\{\lambda\} is a unit clause consisting of just a single literal \lambda
a CNF formula \alpha is a set \alpha = \wedge_{i\leq n}\;\kappa_i represented as \alpha = \{\kappa_i|i \leq n \}
a clause \kappa is called \lambda-positive if \lambda \in \kappa
a clause \kappa is called \lambda-negative if \neg \lambda \in \kappa
a clause \kappa is called \lambda-neutral if \kappa is neither \lambda-positive nor \lambda-negative
if \alpha is a set of clauses, \alpha_\lambda^+ is the set of \lambda-positive clauses of \alpha, \alpha_\lambda^- is the set of \lambda-negative clauses of \alpha, and \alpha_\lambda^0 is the set of \lambda-neutral clauses of \alpha.
At first, I was reading \text{POS}_\lambda(\alpha) as the union of the \lambda-neutral clauses of \alpha with the \lambda-positive clauses of \alpha but excluding the unit clause \{\lambda\}. But apparently it is intended to be read as the union of the \lambda-neutral clauses of \alpha with the \lambda-positive clauses of \alpha but with ALL of the \lambda terms EXCLUDED from those clauses.
WHY is it read that way? Or, to put it another way, why was it not written as \text{POS}_\lambda(\alpha) = \alpha_\lambda^0 \cup \{\kappa - \lambda|\kappa \in \alpha_\lambda^+\}. (Why did they put their \lambda in brackets {}?) And how would you write set-builder notation for "the \lambda-positive clauses of \alpha but excluding just the unit clause \{\lambda\}."
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.
\text{POS}_\lambda(\alpha) = \alpha_\lambda^0 \cup \{\kappa - \{\lambda\}|\kappa \in \alpha_\lambda^+\}
where:
\lambda is a literal
\kappa is an \vee clause with the set \kappa = \vee_{j\leq m}\;\lambda_j represented as \kappa = \{\lambda_j|j \leq m \}
\{\lambda\} is a unit clause consisting of just a single literal \lambda
a CNF formula \alpha is a set \alpha = \wedge_{i\leq n}\;\kappa_i represented as \alpha = \{\kappa_i|i \leq n \}
a clause \kappa is called \lambda-positive if \lambda \in \kappa
a clause \kappa is called \lambda-negative if \neg \lambda \in \kappa
a clause \kappa is called \lambda-neutral if \kappa is neither \lambda-positive nor \lambda-negative
if \alpha is a set of clauses, \alpha_\lambda^+ is the set of \lambda-positive clauses of \alpha, \alpha_\lambda^- is the set of \lambda-negative clauses of \alpha, and \alpha_\lambda^0 is the set of \lambda-neutral clauses of \alpha.
At first, I was reading \text{POS}_\lambda(\alpha) as the union of the \lambda-neutral clauses of \alpha with the \lambda-positive clauses of \alpha but excluding the unit clause \{\lambda\}. But apparently it is intended to be read as the union of the \lambda-neutral clauses of \alpha with the \lambda-positive clauses of \alpha but with ALL of the \lambda terms EXCLUDED from those clauses.
WHY is it read that way? Or, to put it another way, why was it not written as \text{POS}_\lambda(\alpha) = \alpha_\lambda^0 \cup \{\kappa - \lambda|\kappa \in \alpha_\lambda^+\}. (Why did they put their \lambda in brackets {}?) And how would you write set-builder notation for "the \lambda-positive clauses of \alpha but excluding just the unit clause \{\lambda\}."
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.
