let set_hard_constraints solver pool =
  let globalid = (Array.length pool) - 1 in
  match pool.(globalid) with
  |(ll,[]) when not(List.exists (fun l -> (List.length l) < 2) ll) -> begin
      let req = Diagnostic_int.Sng (None,globalid) in
      let res = solve solver req in
      begin match res with
      |Failure _ -> ()
      |Success(f_int) -> 
          List.iter (fun i -> 
            S.add_rule solver.constraints [|S.lit_of_var i true|] [];
          )(f_int ())
      end;
      true
  end
  |-> false