SMT-Solver se puede usar para resolver restricciones. Como sabemos, los solucionadores de CSP también sirven para la resolución de restricciones durante muchos años. Entonces, ¿cuál es la ventaja del solucionador de SMT sobre los solucionadores de CSP?¿Cuál es la ventaja de SMT-Solver sobre CSP-Solver en la resolución de restricciones?
Eso depende completamente de lo que quieras hacer. Puede traducir ambos a SAT y resolver problemas de restricción como un problema SAT. Los solucionadores de restricciones suelen ofrecer el mayor nivel de abstracción cuando se trata de modelar el problema. Los solucionadores de SAT son muy rápidos, pero dependiendo de su problema, un SMT o un solucionador de restricciones podría ser más rápido.
No hay una respuesta general a su pregunta. Depende de su caso de uso particular.
Sí, tiene usted razón, gracias ~ ¿Y quiero saber cuándo los solucionadores de SMT se ejecutan más rápido que los solucionadores de CSP? ¿o qué tipo de problemas son más adecuados para los solucionadores de SMT y, a la inversa? ¿Pueden resolver los solucionadores de SMT los problemas de optimización, que los solucionadores de CSP pueden manejar bien? – user1393905
Ambas restricciones y SMT pueden ocuparse de los problemas de optimización, aunque creo que la compatibilidad con esto en los solucionadores reales es más común en las limitaciones. No hay reglas establecidas cuando SMT/constraints/SAT es mejor/más rápido/... Realmente depende del problema real que intentas resolver. –
OK, muchas gracias ~ – user1393905