Qu'est-ce que le solveur OR-Tools CP-SAT ?
OR-Tools CP-SAT (Constraint Programming SAT) est un solveur de contraintes très performant développé par Google. Il est utilisé pour résoudre efficacement des problèmes complexes en optimisation et satisfaction de contraintes. On le retrouve dans des applications d'ordonnancement, d'affectation de ressources et d'autres problèmes combinatoires.
ORTools permet de modéliser des problèmes de décision sur des domaines finis, à l'aide de variables entières, de variables booléennes et de clauses. La librairie dispose d'un large panel de contraintes, dont des contraintes globales (alldifferent, sum, circuit, cumulative, regular, table, reservoir, etc.).
CPSAT est une librairie open source écrite en C++, avec des APIs en Java, Python et C#.
Un solveur de contraintes hybride et performant
OR-Tools CP-SAT combine différentes approches : Programmation Par Contraintes (CP), SAT, mais aussi de la Programmation Linéraire. L'hybridation CP-SAT est basée sur le framework de Génération Paresseuse de Clauses (LCG), mis en avant par le solveur Chuffed, qui aide le solveur a analyser ses propres conflits durant la recherche d'une solution afin de mieux apprendre de ses erreurs. La Programmation Linéaire quant à elle aide le solveur à mieux exploiter la fonction d'optimisation.
Le solveur utilise par défaut un Portfolio de solveurs permettant de combiner simultanément différentes configurations afin de résoudre le problème le plus efficacement possible.
Quelle différence entre OR-Tools CP-SAT et Choco Solver ?
Les deux solveurs sont d'excellente qualité et ont de nombreuses fonctionnalités en commun. Néanmoins, nous considérons que selon un mode de résolution boîte-noire, OR-Tools CP-SAT donne de meilleurs résultats. Inversement, Choco Solver est plus flexible et permet plus facilement d'enrichir le solveur de composants spécifiques (contraintes, heuristiques), permettant in fine d'obtenir de meilleurs résultats dans de nombreux cas. Le choix du meilleur solveur dépend donc de l'application et de son contexte. Nous accompagnons nos clients avec les deux solveurs, que nous comparons régulièrements sur leurs données.