Problème — MAX2SAT : du hasard au déterminisme

1. L'espérance conditionnelle se calcule exactement, et c'est le point de départ. Fixons une affectation partielle $\sigma$ des premières variables. Une clause est fausse sous $\sigma$ complétée au hasard si et seulement si aucun de ses littéraux n'est déjà vrai, et si tous ses littéraux non encore fixés tombent du mauvais côté. D'où, pour une clause $c$ :

$$\mathrm{Pr}[c\text{ fausse}\mid \sigma ]=\{\begin{array}{ll}0& \text{si un litteˊral de }c\text{ est deˊjaˋ vrai sous }\sigma ,\\ 2^{-r}& \text{sinon, ouˋ }r\text{ est le nombre de litteˊraux non fixeˊs de }c.\end{array}$$

(* Esperance du nombre de clauses satisfaites, les variables non fixees etant
   tirees a pile ou face. fixe.(i) = Some b si x_i vaut b, None sinon.
   Complexite : O(taille de la formule). *)
let esperance clauses fixe =
  Array.fold_left (fun acc cl ->
    let p_fausse = Array.fold_left (fun q (i, positif) ->
      match fixe.(i) with
      | None -> q *. 0.5                       (* litteral libre : une chance sur deux *)
      | Some b -> if b = positif then 0.0 else q   (* deja vrai : clause satisfaite *)
    ) 1.0 cl in
    acc +. (1.0 -. p_fausse)) 0.0 clauses