Nombre de modèles

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

On parcourt l'arbre des $2^n$ valuations en additionnant les contributions (comme le comptage de sous-ensembles du chapitre 11), au lieu de s'arrêter à la première. Une tautologie a $2^n$ modèles, une contradiction $0$.