Importance de la sémantique dans le codage CNF de contraintes de cardinalité : application au diagnostic de SED

Le codage d'un problème a un impact énorme sur le temps de calcul en SAT : un solveur SAT peut résoudre très facilement un problème codé d'une certaine manière, et éprouver des difficultés pour le même problème codé d'une autre manière. Pire, un codage peut favoriser le temps de calcul d'un solveur, et se montrer au contraire inadapté pour un autre solveur. Dans cet article, nous nous concentrons sur l'expression en CNF de contraintes de cardinalité : étant donné un ensemble V de variables propositionelles, étant donnée une valeur entière k, exactement k variables de V doivent être évaluées à vrai. Nous proposons de nouvelles manières de modéliser ces contraintes en cherchant à grouper les variables dont la sémantique est proche. Nous étudions ces codages sur des problèmes de diagnostic de système à événements discrets (SED). Des problèmes jusqu'ici insolubles peuvent être à présent résolus à la fois par des procédures systématiques ou stochastiques. Les résultats mettent également en lumière l'existence d'un codage qui convienne aux deux types d'algorithme