2-SAT

[Miguel Angel]

I have done 2-SAT algorithm, but seems incorrect someone can help me. I'm using not the aproach of making a graph because of the size of vars.

My algo is as following

Code: Select all

procedure 2SAT()
{
For var = 1 to total of variables
   if var found in Clauses then
      val(var) = true
      val(var') = false
      if not contradiction with val(var') then
          remove Clauses containing var
      else
         val(var) = false
         val(var') = true
         if contradiction with val(var) return false
         remove Clauses containing var'
      end if
      if set of Clauses is empty return true;
   end if
end for
return true
}
function contradiction(var_false)
{
  for clause = 1 to total of Clauses
    if var_false is found in clause
       w = clause - var_false;
       if (val(w) = false) return true
       if (val(w) = none)
       {
          val(w) = true
          val(w')= false
          stack.push(w)
       }
    end if
    undo the values of the var's found in stack
return false
}

That's all, but it's not OK, can someone tell me where I'm wrong??. BTW, for conditions involving one single var the condition is (x, 0), where 0 means nothing...so I make a ficticious var=0, where val(0) = false, to force the other literal to be true.

[Cosmin.ro]

Do you still need a solution for this? Please state the constrains.

[Miguel Angel]

Already I don't..
the constraints can be seen as:

(a11 || a12) && ... && (an1 || an2)

But I already know how to solve it, though I haven't programmed