¿Cuándo usar SAT vs Satisfacción de restricción?

Si tengo un problema difícil, un enfoque estándar es expresarlo como una instancia SAT e intentar ejecutar un solucionador SAT en él. Otro enfoque estándar es expresarlo como un problema de satisfacción de restricciones e intentar usar un solucionador CSP. Los dos se sienten de alguna manera vagamente similares en qué tipo de problemas pueden expresarse naturalmente en su formato de entrada.

¿Existen pautas o reglas generales sobre cómo reconocer, para un problema dado, qué enfoque es más probable que produzca buenos resultados? ¿Hay alguna guía que alguien pueda ofrecer sobre qué tipo de problemas pueden ser manejados mejor por los solucionadores SAT que por los solucionadores CSP, o viceversa?

(Obviamente, hay algunos problemas fáciles que pueden resolverse con ambos enfoques. También hay algunos problemas difíciles que no pueden resolverse de manera útil con ninguno de los enfoques. Dejemos eso de lado. El caso en el que la guía es más útil son los problemas en los que SAT los solucionadores funcionan mejor que los solucionadores de CSP, o donde los solucionadores de CSP funcionan mejor que los solucionadores de SAT. ¿Cómo puedo reconocer cuándo un solucionador de SAT es más adecuado que un solucionador de CSP, o cuando un solucionador de CSP es más adecuado que un solucionador SAT, es decir, ¿qué enfoque intentar primero?

Creo que esta es una muy buena pregunta. También podría preguntar: ¿cuándo usar un solucionador SMT? Tengo la sensación de que podría ser difícil determinarlo antes de modelar el problema y ejecutar los solucionadores CSP / SAT / SMT y descubrirlo. ¡Es bien sabido que incluso los solucionadores diferentes funcionan de manera muy diferente en las mismas instancias! Mi intuición también proviene del hecho de que hay potencialmente muchas formas de modelar un problema. Además, hay muchas formas de hacer búsquedas e inferencias, dependiendo de qué tipo de restricciones se usen (si el formalismo en cuestión permite diferentes tipos).

$8 \times 8$$9+9+9=27$$32 \times 32$ Rompecabezas de Sudoku, los solucionadores SAT serían más rápidos que los solucionadores CSP.

Los diferentes formalismos pueden capturar información específica del dominio y explotarla mejor y de diferentes maneras. Para un poco más sobre esto, vea la respuesta y los comentarios aquí .