Re: Optimizing Unit Clause Resolution

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

Date: Mon, 7 Jun 2004 01:46:25 -0600

On Mon, 7 Jun 2004, Russell Easterly wrote:

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

  As it says, those six variables are totally new variables and they are
entirely free. When converting any (a,b,c) clause, six NEW variables are
used each time.
  Verify for yourself that if (a,b,c) is satisfiable, then the left side
has an exactly-one assignment, while if (a,b,c) is not satifiable, then
the left side will be satisfied with some clause having more than one true
variable.

J

Relevant Pages

  • Re: OT - Clinton was NOT offered Bin Laden by Sudan in 1996
    ... Post the link or we will know that you are AGAIN being dishonest! ... I stated that the clause, "read and understand" was above the signature. ... Al Franken's notarized signature is below the clause, ... but you have still FAILED to verify your earlier post! ...
    (alt.guitar.amps)
  • Re: OT - James Tobin, another Republican slimeball gets convicted
    ... The level of detail is purely to expose you, and your lies. ... Then you admitted to the existence of the clause, ... signed, you LYING FOOL. ... Time to verify your claim and PROVE the location of the clause. ...
    (alt.guitar.amps)
  • Re: OT - Clinton was NOT offered Bin Laden by Sudan in 1996
    ... Why do you LIE so obviously? ... I asked you verify THAT claim, ... requires the ball is in your court. ... I qouted the page & the actual clause above the ...
    (alt.guitar.amps)
  • Re: [expect] using the previous output as input
    ... > of an expect send clause? ... Of course you have to verify this regular expression whether it matches your ... expect sets during "expecting". ...
    (comp.lang.tcl)
  • Re: Optimizing Unit Clause Resolution
    ... When converting any clause, six NEW variables are ... Verify for yourself that if is satisfiable, then the left side ... has an exactly-one assignment, while if is not satifiable, then ...
    (comp.theory)