Re: Optimizing Unit Clause Resolution

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

Date: Sat, 5 Jun 2004 16:43:02 -0600

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

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

  • 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. ...
    (comp.theory)
  • 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)
  • 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
    ... >> 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. ...
    (comp.theory)