Satisfacción de restricciones abierta o interactiva

En el pasado, implementé modelos de coordinación utilizando SAT y satisfacción de restricciones regulares como el caballo de batalla principal en sus motores. Continuando en esta línea de trabajo, me gustaría hacer que los modelos sean más interactivos, y la mejor manera que veo de hacerlo es abrir el solucionador de restricciones para que ya no sea un cuadro negro.

Por lo tanto, estoy interesado en aprender más sobre la satisfacción de restricciones donde las restricciones tienen lo que llamaré variables externas , predicados y funciones , es decir, el lenguaje de restricción puede tener predicados como que solo pueden ser satisfecho mediante la consulta de algún agente externo al solucionador, y luego solo cuando es tierra. Un escenario en el que esto es útil es cuando corresponde a algún proceso de decisión externo que no puede incorporarse al solucionador de restricciones. Dichos solucionadores de restricciones podrían llamarse abiertos (ya que las restricciones no se conocen por completo) o interactivas$\mathbf{P}(x)$$x$$\mathbf{P}$ (ya que se requiere interacción para proceder con la satisfacción de restricciones).

Me gustaría saber ambos:

• investigación teórica realizada en esta dirección
• herramientas o bibliotecas que implementan solucionadores de restricciones que permiten la interacción con el mundo externo durante el proceso de resolución de restricciones.

No estoy del todo convencido por el trabajo anterior sobre restricciones abiertas e interactivas.

Un intento de estudiar las preguntas de trazabilidad fue:

• Martin J. Green y Christopher Jefferson, Trazabilidad estructural de restricciones propagadas , CP 2008. doi: 10.1007 / 978-3-540-85958-1_25

aunque este documento deja varias preguntas importantes sin respuesta. El enfoque a través de propagadores en este documento está estrechamente relacionado con las implementaciones existentes de resolución de restricciones.

Creo que el trabajo en SMT (teorías del módulo de satisfacción) también está estrechamente relacionado con su pregunta. Las teorías SMT a menudo están motivadas por problemas de verificación de software y hardware, pero existen teorías con un sabor a IA. Espero con ansias más aplicaciones creadas con SMT como tecnología central, y más trabajo en restricciones aplicando ideas de SMT.

Al leer su pregunta, también estoy de acuerdo en decir que las Teorías del módulo de satisfacción están estrechamente relacionadas con sus necesidades. Sugeriría leer el libro Procedimientos de decisión: un punto de vista algorítmico .

$\mathbf P(x)$

Estoy un poco confundido sobre el término interactivo. Voy a hablar con los demás y agregaré que un solucionador SMT podría ser útil. Para agregar al comentario de Walter Bishop, hay disponibles diapositivas para el libro Procedimientos de decisión (Kroening y Strichman). El tratamiento minucioso de John Harrison en el Manual de lógica práctica y razonamiento automatizado también puede interesarle. El código de ejemplo está disponible en línea.

La princesa de Philipp Ruemmer admite la aritmética con predicados no interpretados, que podrían ajustarse a lo que quiere decir con abierto. Está escrito en Scala, utiliza E-matching en el manejo de la cuantificación y proporciona interpolantes.

¿Qué pasa con las herramientas? Si decide utilizar Prolog como lenguaje de elección, puedo sugerir algunos enfoques de implementación:

• GNU Prolog con es la biblioteca de programación C. Puede llamar a las funciones C desde Prolog y Prolog desde C. Esto le abre muchas posibilidades de ampliar la funcionalidad. Pro: Gnu Prolog es uno de los compiladores de Prolog más rápidos disponibles gratuitamente. Nota: Algunas personas se quejan por la falta de algunos predicados incorporados ... en realidad, la mayoría de ellos se pueden implementar, consulte las capas de compatibilidad de Prolog @SO
• SWI-Prolog tiene una interesante biblioteca de programación, que incluye comunicación de red, soporte de protocolos de memoria intermedia, etc. Y es bastante popular.
• XSB Prolog algunas personas afirman que es el proyecto más interesante en términos de interoperabilidad, que incluye: interfaces de bases de datos, etc.

Prolog es un lenguaje de programación, que es adecuado para hacer muchos tipos de solucionadores (y la mayoría de ellos tienen sus solucionadores de dominio finito).