Satisfiabilité

let satisfiable f =
  let n = nb_variables f in
  let v = Array.make n false in
  let rec essaie i =
    if i = n then evalue v f
    else begin
      v.(i) <- false;
      if essaie (i + 1) then true
      else begin v.(i) <- true; essaie (i + 1) end
    end
  in
  essaie 0

satisfiable (Et (Var 0, Non (Var 0))) vaut false : aucune valuation ne rend x0 et not x0 simultanément vrais — c'est une contradiction.