Satisfação de restrição aberta ou interativa

No passado, implementei modelos de coordenação usando SAT e satisfação regular de restrições como o cavalo de batalha principal em seus motores. Continuando nesta linha de trabalho, gostaria de tornar os modelos mais interativos, e a melhor maneira de fazer isso é abrir o solucionador de restrições para que ele não seja mais uma caixa preta.

Portanto, estou interessado em aprender mais sobre a satisfação de restrições, onde as restrições têm o que chamarei de variáveis , predicados e funções externas , ou seja, a linguagem da restrição pode ter predicados como que só podem ser satisfeitos consultando alguns agente externo ao solucionador e somente quando x estiver aterrado. Um cenário em que isso é útil é sempre que P corresponde a algum processo de decisão externo que não pode ser incorporado ao solucionador de restrições. Esses solucionadores de restrições podem ser chamados de abertos (como as restrições não são totalmente conhecidas) ou interativos$\mathbf{P}(x)$$x$$\mathbf{P}$ (como a interação é necessária para prosseguir com a satisfação da restrição).

Eu gostaria de conhecer os dois:

• pesquisa teórica realizada nessa direção
• ferramentas ou bibliotecas que implementam solucionadores de restrições que permitem a interação com o mundo externo durante o processo de resolução de restrições.

Não estou totalmente convencido pelo trabalho anterior sobre restrições abertas e interativas.

Uma tentativa de estudar as questões de tratabilidade foi:

• Martin J. Green e Christopher Jefferson, Rastreabilidade estrutural de restrições propagadas , CP 2008. doi: 10.1007 / 978-3-540-85958-1_25

embora este artigo deixe várias questões importantes sem resposta. A abordagem via propagadores neste documento está intimamente relacionada às implementações existentes do solucionador de restrições.

Acho que o trabalho em SMT (teorias de módulo de satisfação) também está intimamente relacionado à sua pergunta. As teorias SMT geralmente são motivadas por problemas de verificação de software e hardware, mas existem teorias com sabor de IA. Estou ansioso por mais aplicativos criados com o SMT como a tecnologia principal e por mais trabalho com restrições na aplicação de idéias do SMT.

Lendo sua pergunta, também concordo em dizer que as Teorias do Módulo de Satisfação estão intimamente relacionadas às suas necessidades. Sugiro que leia o livro Procedimentos de Decisão - Um Ponto de Vista Algorítmico .

$\mathbf P(x)$

Estou um pouco confuso sobre o termo interativo. Vou conversar com os outros e acrescentar que um solucionador de SMT pode ser útil. Para adicionar ao comentário de Walter Bishop, lâminas para os procedimentos de decisão (Kroening e Strichman) livro estão disponíveis. O tratamento completo de John Harrison no Manual de lógica prática e raciocínio automatizado também pode lhe interessar. Código de exemplo está disponível online.

A princesa de Philipp Ruemmer suporta aritmética com predicados não interpretados, que podem se encaixar no que você entende por aberto. Está escrito em Scala, usa correspondência E no manuseio de quantificação e fornece interpolantes.

E quanto às ferramentas, se você escolher o Prolog como linguagem de escolha, posso sugerir algumas abordagens de implementação:

• GNU Prolog com é uma biblioteca de programação C. Você pode chamar as funções C do Prolog e Prolog do C. Isso abre muitas possibilidades para ampliar a funcionalidade. Pro: Gnu Prolog é um dos compiladores Prolog mais rápidos disponíveis gratuitamente. Nota: Algumas pessoas reclamam da falta de alguns predicados incorporados ... na verdade, a maioria deles pode ser implementada, consulte as camadas de compatibilidade do Prolog @SO
• SWI-Prolog possui uma biblioteca de programação interessante, incluindo comunicação em rede, suporte a buffers de protocolo, etc. E é bastante popular.
• XSB Prolog algumas pessoas afirmam que é o projeto mais interessante em termos de interoperabilidade - incluindo: interfaces de bancos de dados etc.

Prolog é uma linguagem de programação adequada para a execução de muitos tipos de solucionadores (e a maioria deles possui solucionadores de domínio finito).