Re: Optimizing Unit Clause Resolution

From: Jim Nastos (nastos_at_cs.ualberta.ca)
Date: 06/12/04 

Date: Sat, 12 Jun 2004 02:28:41 -0600

On Sat, 12 Jun 2004, Lash Rambo wrote:

> > where x,y,z,T1,T2,T3 are six new variables per clause.
> > (So n variables, m clauses -> n+6m variables and 4m clauses).
>
> What the hell is this supposed to mean? Is -> supposed to be an
> implication operator? Is the right-hand operand supposed to be (x,y,z)
> or everything after ->? Or is -> instead supposed to be an equivalence
> operator?

I'm using "->" to just loosly indicate <left side> mapping to <right
side>. In the sentence I give above with "->", in english, it says that if
a 3-SAT instance has n variables and m clauses, then the instance of
EXACTLY-ONE-SAT that it maps to will have n+6m variables and 4m clauses.

> What's the significance of using lower-case for some literals
> (a, b, c, x, y, z) and upper-case for others (T1, T2, T3)?

  They are just symbols. Upper or lower cases are irrelevant here.

J