Re: Questions about Parity SAT

Hi,



I am not sure if I've got it right. Your "Parity SAT Positive" is an SAT
instance where each literal exists only in its non-negated form in each
clause it appears? What means that if each clause contains at least one
literal the expression is satisfied?



This reduction may be interesting but I do doubt that it is correct. If you
have described your idea than maybe someone would point where is a flaw.



Imagine we have some SAT (ordinary) instance. Let us denote it as formula F.
Problem question is "Is there at least one assignment". So we create another
instance using brand new (not existing in F) literal r, and ask question if
new formula: (F or r) has odd number of assignments? If we could correctly
answer this question then at the same time we will have answer to our
original SAT instance.



Best regards,



Radek Hofman



.

Relevant Pages

  • Re: Optimizing Unit Clause Resolution
    ... A few unmatched literals is no big deal. ... I was looking for a way to optimize unit clause ... Satisfying a clause forces the assignment of three variables. ... At least two of these forced assignments will satisfy at least ...
    (comp.theory)
  • 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)
  • A Class of 3SAT Solvable in Polytime
    ... If there is an assignment of variables ... in polynomial time. ... Assume we transform every clause in F ... Fhas a satisfying assignment such ...
    (sci.math)
  • A Class of 3SAT Solvable in Polytime
    ... If there is an assignment of variables ... in polynomial time. ... Assume we transform every clause in F ... Fhas a satisfying assignment such ...
    (sci.logic)
  • A Class of 3SAT Solvable in Polytime
    ... If there is an assignment of variables ... in polynomial time. ... Assume we transform every clause in F ... Fhas a satisfying assignment such ...
    (comp.theory)