Le rapport du nombre de clauses (m) au nombre de variables propositionnelles (n) dans une instance CNF, couramment exprimé m/n.

Principe

Capturer la parcimonie globale ou la tension des contraintes en normalisant le nombre de clauses par le nombre de variables ; sert de paramètre de contrôle pour la difficulté empirique et les comportements de type phase.

Démonstration

Une instance 3-SAT avec 450 clauses et 100 variables a une Densité De Clauses 450/100 = 4,5, ce qui la situe par rapport à des régimes où la difficulté empirique change souvent.

Mauvaise application

Employer la Densité De Clauses sans tenir compte de l'hétérogénéité des longueurs de clause, des répétitions de clauses ou de la distribution de fréquence des variables peut mal prédire la difficulté réelle.

Conséquence

Utilisée pour stratifier des familles d'instances et prédire des régimes de satisfaisabilité/insatisfaisabilité et la performance des solveurs ; certaines densités sont corrélées à un coût de recherche empirique plus élevé.

Inversion

Interpréter la densité comme une difficulté absolue ignore les caractéristiques structurelles : une instance de forte densité peut être facile si les clauses sont redondantes ou s'il existe un petit backdoor vers une classe tractable.

Limite

Définie pour la CNF propositionnelle où les nombres de clauses et de variables sont bien définis ; pas directement applicable aux formules quantifiées, aux variantes SAT pondérées ou aux encodages non clausaux sans adaptation.

Tension sémantique

Tension avec la Taille De l'Ensemble Backdoor et la Largeur De Clause : des densités similaires peuvent produire des difficultés très différentes selon la décomposabilité structurelle ou l'arité des clauses.

Synthèse

La Densité De Clauses est une statistique globale normalisée m/n qui résume l'abondance de contraintes par variable ; c'est un paramètre heuristique utile pour prédire la difficulté empirique mais il doit être interprété avec des mesures structurelles.