Re: Optimizing Unit Clause Resolution

From: Lash Rambo (lrambo_at_obmarl.com)
Date: 06/12/04 

Date: Sat, 12 Jun 2004 06:29:27 GMT

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

> On Sat, 5 Jun 2004, Russell Easterly wrote:
>
>> I also show that certain 3SAT problems can be solved in polynomial
>> time. Specifically, any 3SAT instance that has a satisfying
>> assignment, such that exactly one member of each clause is satisfied,
>> can be solved in poly time.
>>
>> For example, the one clause instance (A,B,C) has three such
>> assignements: ~A,~B,C; ~A,B,~C; and A,~B,~C.
>>
>> Is there a well known class of 3SAT problems where exactly one member
>> of each clause can be satisfied?
>
> 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).

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? 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)?

> Note that if the left side is satisfiable then the right side has an
> exactly-one assignment. If the left side is not satisfiable, then the
> right side will have to have at least two true variables in some
> clause.
>
> So, you are claiming to have a polytime solution to an NP-complete
> problem. I checked your page and find it hard to follow. Can you just
> describe the algorithm without going to graphs? You have a cover set
> and an anti-cover set, so can you just concisely write (something like
> pseudo code) which variables get put into which set?
>
> J
>

Relevant Pages

  • 3SAT - A Counting Solver 2
    ... U0,U1,U2 = clause variables ... we talk about the assignment ... represents a satisfying assignment to the ... Adding these new minterms: ...
    (comp.theory)
  • Re: Optimizing Unit Clause Resolution
    ... > Specifically, any 3SAT instance that has a satisfying assignment, such that ... > exactly one member of each clause is satisfied, can be solved in poly time. ... exactly-one assignment. ...
    (comp.theory)
  • Re: Optimizing Unit Clause Resolution
    ... > Specifically, any 3SAT instance that has a satisfying assignment, such that ... > exactly one member of each clause is satisfied, can be solved in poly time. ... exactly-one assignment. ...
    (sci.math)
  • Re: Optimizing Unit Clause Resolution
    ... any 3SAT instance that has a satisfying ... >> assignment, such that exactly one member of each clause is satisfied, ... > exactly-one assignment. ...
    (sci.math)
  • Re: Optimizing Unit Clause Resolution
    ... >> exactly one member of each clause is satisfied, ... > exactly-one assignment. ... Each new assignment leads to two new forced assignments. ... This clause contains more than one member of our trial solution. ...
    (sci.math)
Loading