Problema de satisfacción de restricciones (CSP) versus teoría del módulo de satisfacción (SMT); con una coda en programación de restricciones

¿Alguien se atreve a intentar aclarar cuál es la relación de estos campos de estudio o tal vez incluso dar una respuesta más concreta a nivel de problemas? Como cuál incluye cuál asumiendo algunas formulaciones ampliamente aceptadas. Si entendí esto correctamente, cuando pasas de SAT a SMT básicamente estás entrando en el campo de CSP; viceversa, si limita CSP a booleanos, básicamente está hablando de SAT y quizás de algunos problemas relacionados como #SAT. Creo que esto está claro (por ejemplo, véase el capítulo de Kolaitis y Vardi "Un enfoque lógico para la satisfacción de restricciones" en la teoría de modelos finitos y sus aplicaciones).por Grädel et al.), pero lo que para mí es menos claro es cuándo son las restricciones "módulo a teoría" y cuándo no lo son. ¿SMT siempre implica que la teoría usa solo restricciones de igualdad y desigualdad que siempre están en el campo más amplio de CSP? Por lo que puedo decir, a menudo puede introducir variables de holgura , por lo que la distinción [si existe] es menos que obvia.

El relativamente reciente "Manual de satisfacción" (IOP Press 2009) reúne los problemas SMT y CSP bajo su amplio paraguas de "satisfacción", pero dada la forma en que está estructurado (capítulos escritos por varios autores) realmente no me ayuda a resolver esto .

Yo esperaría la terminología recibe menos confuso cuando se habla de la restricción de programación , que (por analogía con el término '' programación matemática '') Espero que implica minimizar / maximizar alguna función objetivo. Sin embargo, el artículo de Wikipedia sobre programación de restricciones es tan vago que realmente no puedo decir si ocurre este encuadre. Lo que puedo deducir de Essentials of Restraint Programming de Frühwirth and Abdennadher (p. 56) es que un "solucionador de restricciones" generalmente proporciona más que un simple verificador de satisfacción, siendo la simplificación, etc., importante en la práctica.

Aunque esta no es una pregunta real de investigación de la teoría CS, no espero buenas respuestas a esta en el sitio universitario CS.SE dado lo que vi en https://cs.stackexchange.com/questions/14946/distinguish- decision-procedure-vs-smt-solucionador-vs-teorema-probador-vs-restricción-sol (que contiene muchas palabras pero no lo que consideraría una respuesta real, por desgracia).

SAT, CP, SMT, (gran parte) de ASP se ocupan del mismo conjunto de problemas de optimización combinatoria. Sin embargo, se enfrentan a estos problemas desde diferentes ángulos y con diferentes cajas de herramientas. Estas diferencias están en gran medida en cómo cada enfoque estructura la información sobre la exploración del espacio de búsqueda. Mi analogía de trabajo es que SAT es código de máquina, mientras que los otros son idiomas de nivel superior.

$x_1 \lor \overline{x_2} \lor x_3$$\{(x_1,0),(x_2,1),(x_3,0)\}$$x_1$$x_3$$x_2$$x_1 \lor \overline{x_2} \lor x_3 \lor x_4$$x_1 \lor \overline{x_2} \lor x_3 \lor \overline{x_4} \lor x_5$

Se mantiene una aproximación de la estructura de la cláusula para reducir el conjunto de soluciones y ayudar a determinar si este conjunto está vacío. Durante la búsqueda, es posible que algunas tareas parciales no estén incluidas en ninguna solución (incluso si satisfacen individualmente cada una de las restricciones de la instancia). Estos se conocen como nogoods , un término introducido por ("Mr GNU") Stallman y Sussman$x \le 5$$x = 5$. Por lo tanto, no existe una estructura de cláusula general única, sino una asociada con cada elección de representación, dependiendo de lo que representan los singletons (literales) de la estructura de cláusula.

La programación de restricciones (CP) era tradicionalmente una disciplina de IA, con un enfoque en la programación, el calendario y los problemas combinatorios, y por lo tanto tiene un papel central para las variables que pueden tomar más de dos valores (pero generalmente solo finitos). CP ha enfatizado la búsqueda eficiente y, motivado por las aplicaciones tradicionales, ha dado un papel central a la all-differentrestricción (inyectividad), pero también ha desarrollado propagadores eficientes para muchos otros tipos de restricciones. Las definiciones formales de PC han existido desde al menos el papel de Montanari de 1974 Redes de restricciones, con precursores que se remontan incluso antes. Este peso de la historia puede haber contribuido a que la PC se haya quedado rezagada con respecto a otros enfoques en el rendimiento bruto durante la última década. CP mantiene clásicamente una aproximación del complemento de la estructura de la cláusula, a través de un conjunto de dominios activos para las variables. El objetivo es eliminar los valores de los dominios activos, explorando la estructura de la cláusula tratando de asignar valores candidatos a las variables y retrocediendo cuando sea necesario.

Las teorías del módulo de satisfacción (SMT) surgieron de la comunidad de verificación. Cada teoría en un solucionador SMT forma una representación implícita de potencialmente infinitas cláusulas SAT. Las teorías utilizadas con SMT y las restricciones utilizadas en CP reflejan sus diferentes aplicaciones históricas. La mayoría de las teorías que SMT considera tienen que ver con matrices indexadas con enteros, campos cerrados reales, órdenes lineales y similares; Estos surgen del análisis estático de programas (en verificación asistida por computadora) o cuando se formalizan pruebas matemáticas (en razonamiento automatizado). Por el contrario, en el horario y la programación, la restricción de inyectividad es central, y aunque el lenguaje SMTLIB estándar ha tenido una restricción de inyectividad desde su inicio en 2003 (a través dedistinctsímbolo), hasta 2010 los solucionadores SMT solo se implementaron distinctmediante un algoritmo ingenuo. En esa etapa, la técnica de emparejamiento del propagador de CP estándar all-differentse transfirió, con gran efecto cuando se aplicó a grandes listas de variables; vea Un solucionador de restricciones diferente en SMT por Banković y Marić, SMT 2010. Además, la mayoría de los propagadores de CP están diseñados para problemas con dominios finitos, mientras que las teorías SMT estándar tratan dominios infinitos (enteros y más recientemente reales) listos para usar. SMT utiliza una instancia SAT como la aproximación de la estructura de la cláusula, extrayendo nogood cláusulas de las teorías según corresponda. Una buena descripción es las Teorías del módulo de satisfacción: Introducción y aplicaciones de De Moura y Bjørner, doi: 10.1145 / 1995376.1995394.

La programación del conjunto de respuestas (ASP) salió de la programación lógica. Debido a su enfoque en resolver el problema más general de encontrar un modelo estable, y también porque permite la cuantificación universal y existencial, ASP no fue competitiva durante muchos años con CP o SMT.

Formalmente, SAT es CSP en dominios booleanos, pero el enfoque en SAT en el aprendizaje de cláusulas, las buenas heurísticas para la detección de conflictos y las formas rápidas de retroceder son bastante diferentes al enfoque tradicional de CSP en propagadores, estableciendo consistencia y heurística para el orden variable. SAT suele ser extremadamente eficiente, pero para muchos problemas se requiere un gran esfuerzo para expresar primero el problema como una instancia de SAT. El uso de un paradigma de nivel superior como CP puede permitir una expresión más natural del problema, y ​​luego la instancia de CP puede traducirse a SAT a mano o una herramienta puede encargarse de la traducción. Una buena visión general de los aspectos básicos de SAT es Sobre los solucionadores de satisfacción de cláusulas modernas de aprendizaje de Pipatsrisawat y Darwiche, doi: 10.1007 / s10817-009-9156-3 .

Ahora pasemos de las generalidades a los detalles actuales.

Durante la última década, algunas personas en CP han comenzado a centrarse en la generación de cláusulas perezosas (LCG). Esta es esencialmente una forma de atornillar los propagadores de CP utilizando técnicas más flexibles tipo SMT en lugar de la abstracción de dominios activos bastante rígida. Esto es útil porque hay una larga historia de propagadores CP publicados para representar y resolver eficientemente muchos tipos de problemas. (Por supuesto, se lograría un efecto similar mediante un esfuerzo concertado para implementar nuevas teorías para los solucionadores de SMT). LCG tiene un rendimiento que a menudo es competitivo con SMT, y para algunos problemas puede ser superior. Una descripción general rápida es el documento de Stuckey CPAIOR 2010 Lazy Clause Generation: Combinando el poder de la resolución SAT y CP (¿y MIP?) , Doi: 10.1007 / 978-3-642-13520-0_3. También vale la pena leer el documento de posición de García de la Banda, Stuckey, Van Hentenryck y Wallace, que pinta una visión centrada en el CP de The Future of Optimization Technology , doi: 10.1007 / s10601-013-9149-z .

Por lo que puedo decir, gran parte del enfoque de la investigación reciente de SMT parece haberse desplazado a aplicaciones en métodos formales y matemáticas formalizadas. Un ejemplo es la reconstrucción de pruebas encontradas por los solucionadores SMT dentro de sistemas de prueba como Isabelle / HOL, mediante la construcción de tácticas Isabelle / HOL para reflejar las reglas de inferencia en las trazas de prueba SMT; vea Reconstrucción rápida de prueba de estilo LCF para Z3 por Böhmer y Weber en ITP 2010.

Los mejores solucionadores ASP se han desarrollado en los últimos años para ser competitivos con los solucionadores de CP, SMT y SAT solamente. Solo estoy vagamente familiarizado con los detalles de implementación que han permitido a los solucionadores como claspser competitivos, por lo que realmente no puedo compararlos con SMT y CP, pero el cierre anuncia explícitamente su enfoque en aprender nogoods.

Traspasar los límites tradicionales entre estos formalismos es la traducción de representaciones de problemas más abstractas a formalismos implementables de nivel más bajo de manera eficiente. Varios de los principales solucionadores de ASP y CP ahora traducen explícitamente su entrada en una instancia SAT, que luego se resuelve utilizando un solucionador SAT estándar. En CP, el asistente de modelado de restricciones Savile Row utiliza técnicas de diseño de compiladores para traducir los problemas expresados ​​en la esencia del lenguaje de nivel medio en un formalismo de nivel inferior, adecuado para la entrada a solucionadores de CP como Minion o MiniZinc . Savile Row trabajó originalmente con una representación CP como formalismo de bajo nivel, pero introdujo SAT como objetivo en la versión 1.6.2. Además, la esencia lingüística de nivel superiorahora se puede traducir automáticamente a Essence 'con la herramienta Conjure . Al mismo tiempo, los solucionadores solo de SAT de bajo nivel como Lingeling continúan siendo refinados cada año, más recientemente alternando el aprendizaje de cláusulas y las fases de procesamiento; vea la breve descripción de What's Hot in the SAT and ASP Competiciones por Heule y Schaub en AAAI 2015.

La analogía con la historia de los lenguajes de programación parece apropiada. SAT se está convirtiendo en una especie de "código de máquina", dirigido a un modelo de exploración de bajo nivel de las cláusulas en la estructura de la cláusula. Los paradigmas abstractos se están volviendo más como lenguajes informáticos de nivel superior, con sus propias metodologías y aplicaciones distintas que son buenos para abordar. Finalmente, la colección cada vez más densa de enlaces entre estas diferentes capas está comenzando a parecerse al ecosistema de optimización del compilador.