¿Qué es el solucionador OR-Tools CP-SAT?
OR-Tools CP-SAT (Constraint Programming SAT) es un solucionador de restricciones muy eficiente desarrollado por Google. Se utiliza para resolver eficazmente problemas complejos en optimización y satisfacción de restricciones. Se encuentra en aplicaciones de programación, asignación de recursos y otros problemas combinatorios.
ORTools permite modelar problemas de decisión sobre dominios finitos, mediante variables enteras, variables booleanas y cláusulas. La librería dispone de un amplio panel de restricciones, incluyendo restricciones globales (alldifferent, sum, circuit, cumulative, regular, table, reservoir, etc.).
CPSAT es una librería open source escrita en C++, con APIs en Java, Python y C#.
Un solucionador de restricciones híbrido y eficiente
OR-Tools CP-SAT combina diferentes enfoques: Programación Por Restricciones (CP), SAT, pero también Programación Lineal. La hibridación CP-SAT se basa en el framework de Generación Perezosa de Cláusulas (LCG), destacado por el solucionador Chuffed, que ayuda al solucionador a analizar sus propios conflictos durante la búsqueda de una solución para aprender mejor de sus errores. La Programación Lineal por su parte ayuda al solucionador a explotar mejor la función de optimización.
El solucionador utiliza por defecto un Portfolio de solucionadores que permite combinar simultáneamente diferentes configuraciones para resolver el problema de la manera más eficiente posible.
¿Cuál es la diferencia entre OR-Tools CP-SAT y Choco Solver?
Los dos solucionadores son de excelente calidad y tienen numerosas funcionalidades en común. Sin embargo, consideramos que según un modo de resolución caja-negra, OR-Tools CP-SAT da mejores resultados. Inversamente, Choco Solver es más flexible y permite más fácilmente enriquecer el solucionador con componentes específicos (restricciones, heurísticas), permitiendo finalmente obtener mejores resultados en numerosos casos. La elección del mejor solucionador depende por tanto de la aplicación y su contexto. Acompañamos a nuestros clientes con ambos solucionadores, que comparamos regularmente sobre sus datos.