Une mesure de la taille syntaxique maximale (par exemple le nombre de littéraux dans une clause) des formules intermédiaires ou des clauses apparaissant dans une preuve ; en résolution, il s'agit typiquement de la largeur maximale des clauses rencontrées.

Principe

Capture la complexité combinatoire de pointe des objets intermédiaires : des clauses ou formules plus larges indiquent des combinaisons plus importantes de littéraux à traiter simultanément.

Démonstration

Dans des preuves SAT basées sur la résolution, la largeur de preuve est le nombre maximal de littéraux présents dans toute clause produite lors de la réfutation ; les preuves nécessitant des clauses de grande largeur sont souvent plus difficiles à obtenir.

Mauvaise application

Assimiler largeur faible et facilité pour tous les systèmes ignore les effets d'encodage ; une preuve de faible largeur dans un encodage peut correspondre à une preuve de grande largeur ou longue dans un autre encodage ou système de preuve.

Conséquence

Les bornes inférieures sur la largeur peuvent servir à démontrer des bornes exponentielles sur la longueur de preuve en résolution ; maîtriser la largeur est une technique clé pour concevoir des algorithmes paramétrés ou à complexité fixe par paramètre (FPT).

Inversion

On peut au contraire considérer la largeur moyenne ou le nombre total de symboles pour mettre en avant l'encombrement global des formules plutôt que la largeur maximale, ce qui déplace l'attention de l'explosion intermédiaire pire-cas vers le coût agrégé.

Limite

La largeur est liée à la représentation choisie (clauses, séquents, formules) et à l'unité syntaxique comptée (littéraux vs atomes vs symboles) ; elle ne mesure pas directement les étapes séquentielles ou la mémoire sauf si elle est combinée à d'autres métriques.

Tension sémantique

Est en tension avec la longueur et l'espace de preuve : des preuves étroites peuvent rester longues ou consommatrices d'espace, et des preuves de faible longueur peuvent nécessiter des formules intermédiaires larges ; la largeur isole la demande combinatoire simultanée.

Synthèse

La largeur de preuve quantifie la charge combinatoire maximale produite simultanément par une preuve ; utilisée avec la longueur et l'espace elle aide à prévoir les goulets d'étranglement de la recherche et guide des transformations ou encodages qui maintiennent les représentations intermédiaires petites.