Logique propositionnelle

Le programme est explicite deux fois : « les formules sont des données informatiques », et « on implémente uniquement les formules propositionnelles sous forme d'arbres ».

type formule =
  | Var of string
  | Non of formule
  | Et of formule * formule
  | Ou of formule * formule
  | Implique of formule * formule

C'est le type inductif du chapitre chap:induction, et tout ce qui y a été démontré s'applique : les fonctions sur les formules terminent par l'ordre induit, et se prouvent par induction structurelle. Rien n'est à réapprendre.

Le programme le dit : ce sont des « notions que l'on retrouve dans la pratique de la programmation ». Dans let f x = x + a, le $x$ est lié par fun, le $a$ est libre et va chercher sa valeur ailleurs. Renommer un $x$ lié ne change rien ; renommer un $a$ libre change tout. C'est le même phénomène, et le même piège.

Les deux dernières lignes de la colonne $a\to b$ déconcertent : une implication de prémisse fausse est vraie. C'est pourtant le seul choix cohérent. « Si $n$ est divisible par $4$, alors $n$ est pair » doit être vraie pour tout $n$, y compris $n=3$, où prémisse et conclusion sont toutes deux fausses.

Retenez la lecture opérationnelle : $a\to b$ n'est fausse que dans un seul cas, celui où l'on a promis $b$ en ayant $a$, et où $b$ n'est pas là.

Elle transforme « prouver que $\phi$ est toujours vraie » en « montrer que $\neg \phi$ n'a aucun modèle ». Autrement dit : tout problème de validité se ramène à sat. C'est ce qui donne à sat son statut, et c'est aussi ce qui rend le chapitre chap:deduction nécessaire — car chercher un modèle coûte $2^n$.

$p\wedge q$ et $q\wedge p$ sont équivalentes et ne sont pas égales : leurs arbres diffèrent. Un programme qui teste l'égalité structurelle de deux formules ne teste pas leur équivalence — et tester l'équivalence coûte, dans l'état des connaissances, un temps exponentiel.

Le programme demande ce lien, et il est direct : chaque ligne de la table de vérité où la formule vaut $V$ donne une conjonction de la fnd. Pour $\phi =p\leftrightarrow q$, les lignes vraies sont $(V,V)$ et $(F,F)$ :

$$p\leftrightarrow q\equiv (p\wedge q)\vee (\neg p\wedge \neg q).$$

Toute formule admet donc une fnd — et le procédé le montre — mais cette fnd a autant de termes que la table a de lignes vraies, donc jusqu'à $2^n$.

Le programme demande un « exemple de formule dont la taille des formes normales est exponentiellement plus grande ». En voici un, et il est bref :

$${\phi }_n=(p_1\wedge q_1)\vee (p_2\wedge q_2)\vee \cdots \vee (p_n\wedge q_n).$$

Elle est déjà en fnd et sa taille est linéaire. Sa fnc, en revanche, s'obtient en distribuant : il faut choisir un littéral dans chacun des $n$ groupes, ce qui donne

$$\underset{(x_1,\dots ,x_n)\in \{p_i,q_i\}}{\bigwedge }(x_1\vee x_2\vee \cdots \vee x_n)\text{soit }{2}^n\text{ clauses.}$$

Pour $n=20$ : une formule de $40$ variables devient un million de clauses. Une transformation qui préserve la sémantique peut détruire l'efficacité, et c'est pourquoi les solveurs réels emploient des transformations qui ajoutent des variables au lieu de distribuer.

Parce que les solveurs sat modernes traitent couramment des instances à des millions de clauses, et que l'on gagne à écrire des contraintes plutôt qu'un algorithme. C'est le paradigme déclaratif du chapitre chap:algo-prog : on dit ce qu'on veut, un moteur cherche. Le prix à payer est le pire cas exponentiel — que le chapitre chap:decidabilite justifiera.

• Une formule est un arbre — un type inductif —, et tout le chapitre chap:induction s'y applique.
• Syntaxe ($=$, les arbres) et sémantique ($\equiv$, les tables) ne se confondent jamais.
• Tautologie, satisfiabilité et antilogie se ramènent l'une à l'autre par la négation — et donc à sat.
• Toute formule a une fnd lisible dans sa table de vérité, mais la mise en forme normale peut faire passer une taille linéaire à $2^n$.
• Quine est un retour sur trace, et c'est la simplification qui le rend utilisable. $2$-sat est linéaire, $3$-sat est np-complet.