Solve 2-SAT (boolean satisfiability)
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