let is_solvable formula =
   (* get all the variables*)
   let vars = find_vars formula in
   (* functions for the search using the uninf_search part of this lib *)
   (* Nodes of the search space are represented as a tuple of the unbound variables
   and a model containing the bindings for the bound ones*)
   let childgen incomplete =
      (* see if we can bind a variable *)
      match incomplete with
         (*bind it to true and false and remove it from the list of unbound vars *)
         (var :: vars , model) -> [(vars, assign ~var true model);
                                               (vars, assign ~var false model)]
      | ([], _) -> [];
   and
      goaltest incomplete =
         (* as long as there are unbound variables we cannot have a solution *)
         match incomplete with
            ([], model) -> solve formula model
         | _ -> false
   and 
      combinator a b c = 
         (*just see if we have a solution and return the bindings in that case *)
         if b then 
         (
            let (_,res) = a in
            Some res
          )
         else
            c
   in
   let  res = Uninf_search.dfsearch ~start:(vars,empty) ~childgen ~goaltest ~combinator in 
   res