Solve 2-SAT (boolean satisfiability) The general SAT (boolean satisfiability) problem is NP-complete.  But 2-SAT, where each clause has only 2 variables, is in P.  Write a solver for 2-SAT.

Input:

A 2-SAT instance, encoded in CNF as follows.  The first line contains V, the number of boolean variables and N, the number of clauses.  Then N lines follow, each with 2 nonzero integers representing the literals of a clause.  Positive integers represent the given boolean variable and negative integers represent the variable's negation.

Example 1

input

4 5
1 2
2 3
3 4
-1 -3
-2 -4


which encodes the formula (x1 or x2) and (x2 or x3) and (x3 or x4) and (not x1 or not x3) and (not x2 or not x4).

The only setting of the 4 variables that makes the whole formula true is x1=false, x2=true, x3=true, x4=false, so your program should output the single line

output

0 1 1 0


representing the truth values of the V variables (in order from x1 to xV).  If there are multiple solutions, you may output any nonempty subset of them, one per line.  If there is no solution, you must output UNSOLVABLE.

Example 2

input

2 4
1 2
-1 2
-2 1
-1 -2


output

UNSOLVABLE


Example 3

input

2 4
1 2
-1 2
2 -1
-1 -2


output

0 1


Example 4

input

8 12
1 4
-2 5
3 7
2 -5
-8 -2
3 -1
4 -3
5 -4
-3 -7
6 7
1 7
-7 -1


output

1 1 1 1 1 1 0 0
0 1 0 1 1 0 1 0
0 1 0 1 1 1 1 0


(or any nonempty subset of those 3 lines)

Your program must handle all N,V &lt; 100 in a reasonable time.  Try this example to make sure your program can handle a big instance.  Smallest program wins.
Haskell, 278 characters

(∈)=elem
r v[][]=[(&gt;&gt;=(++" ").show.fromEnum.(∈v))]
r v[]c@(a:b:_)=r(a:v)c[]++r(-a:v)c[]++[const"UNSOLVABLE"]
r v(a:b:c)d|a∈v||b∈v=r v c d|(-a)∈v=i b|(-b)∈v=i a|1&lt;3=r v c(a:b:d)where i w|(-w)∈v=[]|1&lt;3=r(w:v)(c++d)[]
t(n:_:c)=(r[][]c!!0)[1..n]++"\n"
main=interact$t.map read.words


Not brute force. Runs in polynomial time. Solves the hard problem (60 variables, 99 clauses) quickly:

&gt; time (runhaskell 1933-2Sat.hs &lt; 1933-hard2sat.txt)
1 1 1 0 0 0 0 0 0 1 1 0 0 1 0 1 1 1 0 1 1 0 0 1 0 0 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 0 1 0 1 1 1 1 0 

real 0m0.593s
user 0m0.502s
sys  0m0.074s


And actually, most of that time is spent compiling the code! 

Full source file, with test cases and quick-check tests available.

Ungolf'd:

-- | A variable or its negation
-- Note that applying unary negation (-) to a term inverts it.
type Term = Int

-- | A set of terms taken to be true.
-- Should only contain  a variable or its negation, never both.
type TruthAssignment = [Term]

-- | Special value indicating that no consistent truth assignment is possible.
unsolvable :: TruthAssignment
unsolvable = [0]

-- | Clauses are a list of terms, taken in pairs.
-- Each pair is a disjunction (or), the list as a whole the conjuction (and)
-- of the pairs.
type Clauses = [Term]

-- | Test to see if a term is in an assignment
(∈) :: Term -&gt; TruthAssignment -&gt; Bool
a∈v = a `elem` v;

-- | Satisfy a set of clauses, from a starting assignment.
-- Returns a non-exhaustive list of possible assignments, followed by
-- unsolvable. If unsolvable is first, there is no possible assignment.
satisfy :: TruthAssignment -&gt; Clauses -&gt; [TruthAssignment]
satisfy v c@(a:b:_) = reduce (a:v) c ++ reduce (-a:v) c ++ [unsolvable]
  -- pick a term from the first clause, either it or its negation must be true;
  -- if neither produces a viable result, then the clauses are unsolvable
satisfy v [] = [v]
  -- if there are no clauses, then the starting assignment is a solution!

-- | Reduce a set of clauses, given a starting assignment, then solve that
reduce :: TruthAssignment -&gt; Clauses -&gt; [TruthAssignment]
reduce v c = reduce' v c []
  where
    reduce' v (a:b:c) d
        | a∈v || b∈v = reduce' v c d
            -- if the clause is already satisfied, then just drop it
        | (-a)∈v = imply b
        | (-b)∈v = imply a
            -- if either term is not true, the other term must be true
        | otherwise = reduce' v c (a:b:d)
            -- this clause is still undetermined, save it for later
        where 
          imply w
            | (-w)∈v = []  -- if w is also false, there is no possible solution
            | otherwise = reduce (w:v) (c++d)
                -- otherwise, set w true, and reduce again
    reduce' v [] d = satisfy v d
        -- once all caluses have been reduced, satisfy the remaining

-- | Format a solution. Terms not assigned are choosen to be false
format :: Int -&gt; TruthAssignment -&gt; String
format n v
    | v == unsolvable = "UNSOLVABLE"
    | otherwise = unwords . map (bit.(∈v)) $ [1..n]
  where
    bit False = "0"
    bit True = "1"

main = interact $ run . map read . words 
  where
    run (n:_:c) = (format n $ head $ satisfy [] c) ++ "\n"
        -- first number of input is number of variables
        -- second number of input is number of claues, ignored
        -- remaining numbers are the clauses, taken two at a time


In the golf'd version, satisfy and format have been rolled into reduce, though in order to avoid passing n, reduce returns a function from a list of variables ([1..n]) to the string result.




Edit: (330 -> 323) made s an operator, better handling of the newline
Edit: (323 -> 313) first element from a lazy list of results is smaller than a custom short-circuit operator; renamed main solver function 'cause I like using ∮ as an operator!
Edit: (313 -> 296) keep clauses as a single list, not a list of lists; process it two elements at a time
Edit: (296 -> 291) merged the two mutually recursive functions; it was cheaper to inline ★ so test now renamed ∈
Edit: (291 -> 278) inlined output formatting into results generation