# 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 < 100 in a reasonable time. Try this example to make sure your program can handle a big instance. Smallest program wins.

• You mention that 2-SAT is in P, but not that it is a requirement that the solution must run in polynomial time ;-) – Timwi Apr 4 '11 at 17:22
• @Timwi: No, but it has to handle V=99 in a reasonable time... – Keith Randall Apr 4 '11 at 18:10

(∈)=elem
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. 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

# 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 (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.
• You could remove the parens around the rank arguments. "(_,1) to "_ 1. #: would work without the left argument. – isawdrones Apr 4 '11 at 18:41
• @isawdrones: I think the traditional response would be to crush my spirit by producing an answer half as long. "Scream and leap", as the Kzin would say. Thanks, though, that eliminates 10-odd characters... I might get under 100 when I get back to it. – Jesse Millikan Apr 4 '11 at 18:58
• +1 for the nice and detailed explanation, very fascinating read! – Timwi Apr 4 '11 at 19:20
• Probably won't handle N=V=99 in a reasonable time. Try the big example I just added. – Keith Randall Apr 5 '11 at 16:29

## K - 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"]

• Nice, I didn't know there was a free K implementation. – Jesse Millikan Apr 4 '11 at 23:59
• Probably won't handle N=V=99 in a reasonable time. Try the big example I just added. – Keith Randall Apr 5 '11 at 16:30

## 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 :(

n,v=gets.split
d=[]
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'

• Probably won't handle N=V=99 in a reasonable time. Try the big example I just added. – Keith Randall Apr 5 '11 at 16:29

# 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 [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).

• Nice to see the OCaml version! It makes the start of a nice Rosetta Stone for functional programs. Now if we could get Scala and F# versions... -- As for the algorithm - I didn't see that PDF until you mentioned it here! I based my implementation off of the Wikipedia page's description of "Limited Backtracking". – MtnViewMark Apr 12 '11 at 19:50