Resumen: En este trabajo, proponemos formulaciones de restricciones genéricas que pueden modelar una amplia gama de restricciones de programación del mundo real. Luego, las limitaciones genéricas se formulan como problemas SMT y MILP y se utilizan para comparar los respectivos solucionadores de última generación, Z3 y Gurobi, en problemas de lista de inspiración académica y del mundo real. Los resultados experimentales muestran cómo cada solucionador se destaca por ciertos tipos de problemas; El solucionador MILP generalmente funciona mejor cuando el problema es altamente limitado o no factible, mientras que el solucionador SMT funciona mejor de lo contrario. En los problemas inspirados en el mundo real que contienen un conjunto más variado de turnos y personal, el solucionador SMT sobresale. Además, se observó durante la experimentación que el solucionador SMT era más sensible a la forma en que se formularon las restricciones genéricas, lo que requiere una consideración y experimentación cuidadosa para lograr un mejor rendimiento. Concluimos que los métodos basados en SMT presentan una vía prometedora para futuras investigaciones dentro del dominio de la programación de personal.
Publicado Originalme en rss.arxiv.org El 15 de mayo de 2025.
Ver Fuente Original
