Minimum Satisfiability and its Applications
Résumé
We define solving techniques for the Minimum Satisfiability Problem (MinSAT), propose an efficient branch-and-bound algorithm to solve the Weighted Partial MinSAT problem, and report on an empirical evaluation of the algorithm on Min-3SAT, MaxClique, and combinatorial auction problems. Techniques solving MinSAT are substantially different from those for the Maximum Satisfiability Problem (MaxSAT). Our results provide empirical evidence that solving combinatorial optimization problems by reducing them to MinSAT may be substantially faster than reducing them to MaxSAT, and even competitive with specific algorithms. We also use MinSAT to study an interesting correlation between the minimum number and the maximum number of satisfied clauses of a SAT instance.
Nous proposons, dans cet article, de placer le problème de satisfiabilité minimale (MinSAT) sur le devant de la scène. Pour cela, un algorithme efficace de type {em branch-and-bound} pour résoudre le problème MinSAT partiel avec pondération est introduit, permettant du même coup une évaluation empirique de cet algorithme pour les cas Min-3SAT aléatoires, MaxClique et pour les problèmes d'enchères combinatoires. Les techniques employées pour résoudre MinSAT se démarquent de celles utilisées pour le problème de satisfiabilité maximale (MaxSAT), qui a lui été très étudié. Nos résultats démontrent de manière empirique que, notamment sur les problèmes d'enchères combinatoires, une réduction du problème initial à MinSAT peut être plus intéressante qu'une réduction à MaxSAT, ou même que l'utilisation de méthodes dédiées. Nous étendons par ailleurs ce travail en montrant une corrélation entre le nombre minimal et le nombre maximal de clauses satisfaites dans une instance SAT aléatoire donnée.