2-SAT

Let's talk about algorithms!

Moderator: Board moderators

Post Reply
Miguel Angel
Learning poster
Posts: 60
Joined: Tue Aug 13, 2002 2:39 am
Location: Mexico

2-SAT

Post by 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.
:D Miguel & Marina :D
Cosmin.ro
Learning poster
Posts: 95
Joined: Thu Aug 21, 2003 12:02 am

Post by Cosmin.ro »

Do you still need a solution for this? Please state the constrains.
Miguel Angel
Learning poster
Posts: 60
Joined: Tue Aug 13, 2002 2:39 am
Location: Mexico

Well..

Post by 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 :)
:D Miguel & Marina :D
Post Reply

Return to “Algorithms”