Re: Optimizing Unit Clause Resolution

From: Russell Easterly (logiclab_at_comcast.net)
Date: 06/07/04 

Date: Mon, 7 Jun 2004 08:13:59 -0700

"Jim Nastos" <nastos@cs.ualberta.ca> wrote in message
news:Pine.LNX.4.44.0406051619160.32381-100000@tees.cs.ualberta.ca...

> The well-known problem "exactly-one-SAT" is NP-complete and the
> reduction is straight from 3-SAT:
>
> To map a 3-SAT instance to an instance of EXACTLY-ONE-(OutOf3)-SAT:
>
> (a,b,c) -> (x,y,z) ^ (x, ~a, T1) ^ (y, ~b, T2) ^ (z, ~c, T3)
>
> where x,y,z,T1,T2,T3 are six new variables per clause.
> (So n variables, m clauses -> n+6m variables and 4m clauses).
>

Would you please give a brief description of how x,y,z,T1,T2, and T3
are defined. I couldn't find a good description on the web.

Russell
- 2 many 2 count