let rec int_to_nat = function 
    0 -> O
  | n -> S (int_to_nat (n-1))

let rec nat_to_int = function
    O -> 0
  | S n -> 1 + nat_to_int n

let read fname =
  let inf = open_in fname in

  let rec readHeader () =
    let s = input_line inf in
    if s.[0] = 'c' then
      readHeader ()
    else
      s in

  let header = readHeader () in

  let vars, clauses = Scanf.sscanf header "p cnf %d %d" (fun vars clauses -> (vars, clauses)) in

  let rec readClauses clauses =
    match clauses with
      0 -> Nil
    | _ ->
	let rec readLits () =
	  let n = Scanf.fscanf inf " %d" (fun n -> n) in
	  match n with
	    0 -> Nil
	  | _ ->
	      Cons ((if n > 0 then
		Pair (True, int_to_nat n)
	      else
		Pair (False, int_to_nat (-n))),
		    readLits ()) in
	Cons (readLits (), readClauses (clauses - 1)) in
  
  let r = readClauses clauses in
  close_in inf;
  vars, r
      
let solve' fname =
  let vars, clauses = read fname in
  boundedSat (int_to_nat (vars + 1)) clauses

let rec iter f = function
    Nil -> ()
  | Cons (h, t) -> f h; iter f t

let unbool = function
    True -> true
  | False -> false

let solve fname =
  match solve' fname with
    None -> print_endline "Timeout!"
  | Some (Inleft al) ->
      print_endline "Satisfiable!";
      iter (fun (Pair (b, v)) ->
	Printf.printf "%4d => %b\n" (nat_to_int v) (unbool b)) al
  | Some Inright ->
      print_endline "Unsatisfiable"