[Question]
  [
The general [SAT](http://en.wikipedia.org/wiki/Boolean_satisfiability_problem) (boolean satisfiability) problem is NP-complete. But [2-SAT](http://en.wikipedia.org/wiki/2-satisfiability), where each clause has only 2 variables, is in [P](http://en.wikipedia.org/wiki/P_%28complexity%29). Write a solver for 2-SAT.
Input:
A 2-SAT instance, encoded in [CNF](http://en.wikipedia.org/wiki/Conjunctive_normal_form) 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 < 100 in a reasonable time. Try [this example](http://keithandkatie.com/hard2sat.txt) to make sure your program can handle a big instance. Smallest program wins.
  
[Answer]
## Haskell, 278 characters
```
(∈)=elem
r v[][]=[(>>=(++" ").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<3=r v c(a:b:d)where i w|(-w)∈v=[]|1<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:
```
> time (runhaskell 1933-2Sat.hs < 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](https://bitbucket.org/mtnviewmark/haskell-playground/src/c4dd324f35f7/golf/1933-2Sat.hs).
**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 -> TruthAssignment -> 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 -> Clauses -> [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 -> Clauses -> [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 -> TruthAssignment -> 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
[Answer]
# J, 119 103
```
echo'UNSOLVABLE'"_`(#&c)@.(*@+/)(3 :'*./+./"1(*>:*}.i)=y{~"1 0<:|}.i')"1 c=:#:i.2^{.,i=:0&".;._2(1!:1)3
```
* Passes all test cases. No noticeable runtime.
* Brute force. Passes test cases below, oh, N=20 or 30. Not sure.
* Tested via [completely brain-dead test script](https://gist.github.com/901212) (By visual inspection)
**Edit:** Eliminated `(n#2)` and thus `n=:`, as well as eliminating some rank parens (thanks, isawdrones). Tacit->explicit and dyadic->monadic, eliminating a few more characters each. `}.}.` to `}.,`.
**Edit:** Whoops. Not only is this a non-solution for large N, but `i. 2^99x` -> "domain error" to add insult to stupidity.
Here's the ungolfed original version and brief explanation.
```
input=:0&".;._2(1!:1)3
n =:{.{.input
clauses=:}.input
cases=:(n#2)#:i.2^n
results =: clauses ([:*./[:+./"1*@>:@*@[=<:@|@[{"(0,1)])"(_,1) cases
echo ('UNSOLVABLE'"_)`(#&cases) @.(*@+/) results
```
* `input=:0&".;._2(1!:1)3` cuts input on newlines and parses numbers on each line (accumulating the results into input).
* n is assigned to `n`, clause matrix assigned to `clauses` (don't need the clause count)
* `cases` is 0..2n-1 converted to binary digits (all test cases)
* `(Long tacit function)"(_,1)` is applied to each case in `cases` with all of `clauses`.
* `<:@|@[{"(0,1)]` gets a matrix of the operands of the clauses (by taking abs(op number) - 1 and dereferencing from case, which is an array)
* `*@>:@*@[` gets clause-shaped array of 'not not' bits (0 for not) via abuse of signum.
* `=` applies the not bits to the operands.
* `[:*./[:+./"1` applies `+.` (and) across the rows of the resulting matrix, and `*.` (or) across the result of that.
* All of those results end up as a binary array of 'answers' for each case.
* `*@+/` applied to results gives a 0 if there are results and 1 if there are none.
* `('UNSOLVABLE'"_)` ``(#&cases) @.(*@+/) results` runs constant function giving 'UNSOLVABLE' if 0, and a copy of each 'solution' element of cases if 1.
* `echo` magic-prints the result.
[Answer]
## [K](https://github.com/kevinlawler/kona/) - 89
The same method as the J solution.
```
n:**c:.:'0:`;`0::[#b:t@&&/+|/''(0<'c)=/:(t:+2_vs!_2^n)@\:-1+_abs c:1_ c;5:b;"UNSOLVABLE"]
```
[Answer]
# OCaml + Batteries, 438 436 characters
Requires an OCaml Batteries Included top-level:
```
module L=List
let(%)=L.mem
let rec r v d c n=match d,c with[],[]->[String.join" "[?L:if x%v
then"1"else"0"|x<-1--n?]]|[],(x,_)::_->r(x::v)c[]n@r(-x::v)c[]n@["UNSOLVABLE"]|(x,y)::c,d->let(!)w=if-w%v
then[]else r(w::v)(c@d)[]n in if x%v||y%v then r v c d n else if-x%v then!y else if-y%v then!x else r v c((x,y)::d)n
let(v,_)::l=L.of_enum(IO.lines_of stdin|>map(fun s->Scanf.sscanf s"%d %d"(fun x y->x,y)))in print_endline(L.hd(r[][]l v))
```
I must confess, this is a direct translation of the Haskell solution. In my defense, that in turn is a direct coding of the algorithm [presented here](http://suraj.lums.edu.pk/~cs514s05/data/2SAT.pdf) [PDF], with the mutual `satisfy`-`eliminate` recursion rolled into a single function. An unobfuscated version of the code, minus the use of Batteries, is:
```
let rec satisfy v c d = match c, d with
| (x, y) :: c, d ->
    let imply w = if List.mem (-w) v then raise Exit else satisfy (w :: v) (c @ d) [] in
    if List.mem x v || List.mem y v then satisfy v c d else
    if List.mem (-x) v then imply y else
    if List.mem (-y) v then imply x else
    satisfy v c ((x, y) :: d)
| [], [] -> v
| [], (x, _) :: _ -> try satisfy (x :: v) d [] with Exit -> satisfy (-x :: v) d []
let rec iota i =
    if i = 0 then [] else
    iota (i - 1) @ [i]
let () = Scanf.scanf "%d %d\n" (fun k n ->
    let l = ref [] in
    for i = 1 to n do
        Scanf.scanf "%d %d\n" (fun x y -> l := (x, y) :: !l)
    done;
    print_endline (try let v = satisfy [] [] !l in
    String.concat " " (List.map (fun x -> if List.mem x v then "1" else "0") (iota k))
    with Exit -> "UNSOLVABLE") )
```
(the `iota k` pun I hope you'll forgive).
[Answer]
## Ruby, 253
```
n,v=gets.split;d=[];v.to_i.times{d<<(gets.split.map &:to_i)};n=n.to_i;r=[1,!1]*n;r.permutation(n){|x|y=x[0,n];x=[0]+y;puts y.map{|z|z||0}.join ' 'or exit if d.inject(1){|t,w|t and(w[0]<0?!x[-w[0]]:x[w[0]])||(w[1]<0?!x[-w[1]]:x[w[1]])}};puts 'UNSOLVABLE'
```
But it's slow :(
Pretty readable once expanded:
```
n,v=gets.split
d=[]
v.to_i.times{d<<(gets.split.map &:to_i)} # read data
n=n.to_i
r=[1,!1]*n # create an array of n trues and n falses
r.permutation(n){|x| # for each permutation of length n
    y=x[0,n]
    x=[0]+y
    puts y.map{|z| z||0}.join ' ' or exit if d.inject(1){|t,w| # evaluate the data (magic!)
        t and (w[0]<0 ? !x[-w[0]] : x[w[0]]) || (w[1]<0 ? !x[-w[1]] : x[w[1]])
    }
}
puts 'UNSOLVABLE'
```
]