Programação do conjunto de respostas

Da Wikipédia, a enciclopédia livre
Ir para a navegação Saltar para pesquisar

A programação de conjunto de respostas ( ASP ) é uma forma de programação declarativa orientada para problemas de pesquisa difíceis (principalmente NP-difíceis ) . É baseado na semântica do modelo estável (conjunto de respostas) da programação lógica . No ASP, os problemas de pesquisa são reduzidos a modelos estáveis ​​de computação, e os solucionadores de conjuntos de respostas — programas para gerar modelos estáveis ​​— são usados ​​para realizar a pesquisa. O processo computacional empregado no projeto de muitos solucionadores de conjuntos de respostas é um aprimoramento do algoritmo DPLL e, em princípio, sempre termina (ao contrário da avaliação de consultas Prolog , que pode levar a um loop infinito).

Em um sentido mais geral, ASP inclui todas as aplicações de conjuntos de respostas para representação de conhecimento [1] [2] e o uso de avaliação de consulta no estilo Prolog para resolver problemas que surgem nessas aplicações.

História

O método de planejamento proposto em 1993 por Dimopoulos, Nebel e Köhler [3] é um dos primeiros exemplos de programação de conjuntos de respostas. Sua abordagem é baseada na relação entre planos e modelos estáveis. [4] Soininen e Niemelä [5] aplicaram o que hoje é conhecido como programação de conjuntos de respostas ao problema de configuração do produto . O uso de solucionadores de conjuntos de respostas para busca foi identificado como um novo paradigma de programação por Marek e Truszczyński em um artigo que apareceu em uma perspectiva de 25 anos sobre o paradigma de programação lógica publicado em 1999 [6] e em [Niemelä 1999]. [7] De fato, a nova terminologia de "conjunto de respostas" em vez de "modelo estável" foi proposta pela primeira vez por Lifschitz [8] em um artigo que aparece no mesmo volume retrospectivo do artigo de Marek-Truszczynski.

Resposta definir linguagem de programação AnsProlog

Lparse é o nome do programa que foi criado originalmente como uma ferramenta de aterramento (front-end) para o conjunto de respostas smodels solver . A linguagem que Lparse aceita agora é comumente chamada de AnsProlog, [9] abreviação de Answer Set Programming in Logic . [10] Ele agora é usado da mesma maneira em muitos outros solucionadores de conjuntos de respostas, incluindo assat , clasp , cmodels , gNt , nomore ++ e pbmodels . ( dlv é uma exceção; a sintaxe dos programas ASP escritos para dlv é um pouco diferente.)

Um programa AnsProlog consiste em regras da forma

< cabeça >  :-  < corpo >  .

O símbolo :-("if") é descartado se <body>estiver vazio; tais regras são chamadas de fatos . O tipo mais simples de regras Lparse são regras com restrições .

Uma outra construção útil incluída nesta linguagem é a escolha . Por exemplo, a regra de escolha

{ p , q , r }.

diz: escolha arbitrariamente qual dos átomospara incluir no modelo estável. O programa Lparse que contém esta regra de escolha e nenhuma outra regra tem 8 modelos estáveis ​​- subconjuntos arbitrários de. A definição de um modelo estável foi generalizada para programas com regras de escolha. [11] As regras de escolha também podem ser tratadas como abreviações para fórmulas proposicionais sob a semântica do modelo estável . [12] Por exemplo, a regra de escolha acima pode ser vista como abreviação para a conjunção de três fórmulas " excluídas do meio ":

A linguagem do Lparse nos permite também escrever regras de escolha "restritas", como

1 { p , q , r } 2.

Esta regra diz: escolha pelo menos 1 dos átomos, mas não mais que 2. O significado desta regra sob a semântica do modelo estável é representado pela fórmula proposicional

Os limites de cardinalidade também podem ser usados ​​no corpo de uma regra, por exemplo:

:-  2 { p , q , r }.

Adicionar essa restrição a um programa Lparse elimina os modelos estáveis ​​que contêm pelo menos 2 dos átomos. O significado desta regra pode ser representado pela fórmula proposicional

Variáveis ​​(em maiúsculas, como em Prolog ) são usadas em Lparse para abreviar coleções de regras que seguem o mesmo padrão e também para abreviar coleções de átomos dentro da mesma regra. Por exemplo, o programa Lparse

p ( a ).  p ( b ).  p ( c ). 
q ( X )  :-  p ( X ),  X ! = um .

tem o mesmo significado que

p ( a ).  p ( b ).  p ( c ). 
q ( b ).  q ( c ).

O programa

p ( a ).  p ( b ).  p ( c ). 
{ q ( X ):- p ( X )} 2.

é abreviação para

p ( a ).  p ( b ).  p ( c ). 
{ q ( a ), q ( b ), q ( c )} 2.

Um intervalo é da forma:

( começo .. fim )

onde início e fim são expressões aritméticas de valor constante. Um intervalo é um atalho de notação usado principalmente para definir domínios numéricos de maneira compatível. Por exemplo, o fato

a ( 1..3 ).

é um atalho para

um ( 1 ).  um ( 2 ).  um ( 3 ).

Os intervalos também podem ser usados ​​em corpos de regras com a mesma semântica.

Um literal condicional é da forma:

p ( X ) : q ( X )

Se a extensão de q é {q(a1),q(a2), ... ,q(aN)}, a condição acima é semanticamente equivalente a escrever {p(a1),p(a2), ... , p(aN)} no lugar da condição. Por exemplo,

q ( 1..2 ). 
a  :-  1  { p ( X ) : q ( X )}.

é um atalho para

q ( 1 ).  q ( 2 ). 
a  :-  1  { p ( 1 ),  p ( 2 )}.

Gerando modelos estáveis

Para encontrar um modelo estável do programa Lparse armazenado em arquivo ${filename}usamos o comando

% lparse ${ nome do arquivo }  | modelos

A opção 0 instrui os smodels a encontrar todos os modelos estáveis ​​do programa. Por exemplo, se o arquivo testcontém as regras

1 { p , q , r } 2. 
s  :-  não  p .

então o comando produz a saída

% teste  lparse | smodels 0 
Resposta: 1 
Modelo Estável: qp 
Resposta: 2 
Modelo Estável: p 
Resposta: 3 
Modelo Estável: rp 
Resposta: 4 
Modelo Estável: qs 
Resposta: 5 
Modelo Estável: rs 
Resposta: 6 
Modelo Estável: rqs

Exemplos de programas ASP

Coloração do gráfico

A- coloração de um gráfico é uma funçãode tal modo quepara cada par de vértices adjacentes. Gostaríamos de usar ASP para encontrar um-coloração de um dado gráfico (ou determinar que ele não existe).

Isso pode ser feito usando o seguinte programa Lparse:

c ( 1. . n ).                                           
1  { cor ( X , I )  :  c ( I )}  1  :-  v ( X ).             
:-  cor ( X , I ),  cor ( Y , I ),  e ( X , Y ),  c ​​( I ).

A linha 1 define os númerosser cores. De acordo com a regra de escolha na Linha 2, uma cor únicadeve ser atribuído a cada vértice. A restrição na Linha 3 proíbe atribuir a mesma cor aos vérticesese houver uma aresta ligando-os.

Se combinarmos este arquivo com uma definição de, tal como

v ( 1..100 ).  % 1,...,100 são vértices 
e ( 1 , 55 ).  % existe uma margem de 1 a 55 
.  .  .

e execute smodels nele, com o valor numérico deespecificado na linha de comando, então os átomos do formuláriona saída de smodels representará um-coloração de.

O programa neste exemplo ilustra a organização "gerar e testar" que geralmente é encontrada em programas ASP simples. A regra de escolha descreve um conjunto de "soluções potenciais" — um superconjunto simples do conjunto de soluções para um determinado problema de busca. É seguido por uma restrição, que elimina todas as soluções potenciais que não são aceitáveis. No entanto, o processo de busca empregado por smodels e outros solucionadores de conjuntos de respostas não é baseado em tentativa e erro .

Grande clique

Um clique em um grafo é um conjunto de vértices adjacentes aos pares. O seguinte programa Lparse encontra um clique de tamanhoem um dado gráfico, ou determina que ele não existe:

n  { em ( X )  :  v ( X )}.
:-  em ( X ),  em ( Y ),  v ( X ),  v ( Y ),  X ! = Y ,  não  e ( X , Y ),  não  e ( Y , X ).

Este é outro exemplo da organização de geração e teste. A regra de escolha na Linha 1 "gera" todos os conjuntos que consistem emvértices. A restrição na Linha 2 "elimina" os conjuntos que não são cliques.

Ciclo hamiltoniano

Um ciclo hamiltoniano em um grafo direcionado é um ciclo que passa por cada vértice do grafo exatamente uma vez. O seguinte programa Lparse pode ser usado para encontrar um ciclo hamiltoniano em um determinado grafo direcionado, se ele existir; assumimos que 0 é um dos vértices.

{ em ( X , Y )}  :-  e ( X , Y ).

:-  2  { em ( X , Y )  :  e ( X , Y )},  v ( X ).
:-  2  { em ( X , Y )  :  e ( X , Y )},  v ( Y ).

r ( X )  :-  em ( 0 , X ),  v ( X ).
r ( Y )  :-  r ( X ),  em ( X , Y ),  e ( X , Y ).

:-  não  r ( X ),  v ( X ).

A regra de escolha na Linha 1 "gera" todos os subconjuntos do conjunto de arestas. As três restrições "eliminam" os subconjuntos que não são ciclos hamiltonianos. O último deles usa o predicado auxiliar("é alcançável a partir de 0") para proibir os vértices que não satisfazem esta condição. Este predicado é definido recursivamente nas Linhas 6 e 7.

Este programa é um exemplo da organização mais geral "gerar, definir e testar": inclui a definição de um predicado auxiliar que nos ajuda a eliminar todas as soluções potenciais "ruins".

Análise de dependência

No processamento de linguagem natural , a análise baseada em dependência pode ser formulada como um problema ASP. [13] O código a seguir analisa a frase latina "Puella pulchra in villa linguam latinam discit", "a menina bonita está aprendendo latim na villa". A árvore sintática é expressa pelos predicados arc que representam as dependências entre as palavras da sentença. A estrutura computada é uma árvore enraizada ordenada linearmente.

% ********** frase de entrada ********** 
palavra ( 1 ,  puella ).  palavra ( 2 ,  pulchra ).  palavra ( 3 ,  em ).  palavra ( 4 ,  vila ).  palavra ( 5 ,  linguam ).  palavra ( 6 ,  latina ).  palavra ( 7 ,  discit ). 
% ********** léxico ********** 
1 {  ( X ,  attr( pulcher ,  a ,  fem ,  nom ,  sg )); 
   ( X ,  attr ( pulcher ,  a ,  fem ,  abl ,  sg ))  } 1  :-  palavra ( X ,  pulchra ). 
( X ,  attr ( latinus ,  a ,  fem ,  acc ,  sg ))  :-  palavra ( X,  latino ). 
1 {  ( X ,  attr ( puella ,  n ,  fem ,  nom ,  sg )); 
   ( X ,  attr ( puella ,  n ,  fem ,  abl ,  sg ))  } 1  :-  palavra ( X ,  puella ). 
1 {  ( X ,  attr ( villa ,  n,  fem ,  nom ,  sg )); 
   ( X ,  attr ( villa ,  n ,  fem ,  abl ,  sg ))  } 1  :-  palavra ( X ,  villa ). 
( X ,  attr ( linguam ,  n ,  fem ,  acc ,  sg ))  :-  palavra ( X ,  linguam ). 
( X ,  attr ( discernir ,  v ,  pres ,  3 ,  sg ))  :-  palavra ( X ,  discit ). 
( X ,  attr ( in ,  p ))  :-  palavra ( X ,  in ). 
% ********** regras sintáticas ********** 
0 {  arc ( X ,  Y ,  subj )  } 1  :-  node (X ,  attr ( _ ,  v ,  _ ,  3 ,  sg )),  ( Y ,  attr ( _ ,  n ,  _ ,  nom ,  sg )). 
0 {  arco ( X ,  Y ,  dobj )  } 1  :-  ( X ,  attr ( _ ,  v ,  _ ,  3 ,  sg )), ( Y ,  attr ( _ ,  n ,  _ ,  acc ,  sg )). 
0 {  arc ( X ,  Y ,  attr )  } 1  :-  node ( X ,  attr ( _ ,  n ,  Gender ,  Case ,  Number )),  node ( Y ,  attr ( _ ,  a ,  Gender , Caso ,  Número )). 
0 {  arco ( X ,  Y ,  prep )  } 1  :-  ( X ,  attr ( _ ,  p )),  ( Y ,  attr ( _ ,  n ,  _ ,  abl ,  _ )),  X  <  Y . 
0 {  arco ( X ,  Y ,  adv )  }1  :-  ( X ,  attr ( _ ,  v ,  _ ,  _ ,  _ )),  ( Y ,  attr ( _ ,  p )),  não  folha ( Y ). 
% ********** garantindo a árvore do grafo ********** 
1 {  root ( X ) : node ( X ,  _ )  } 1. 
:-  arc ( X , Z ,  _ ),  arco ( Y ,  Z ,  _ ),  X  ! =  Y. _ 
:-  arco ( X ,  Y ,  L1 ),  arco ( X ,  Y ,  L2 ),  L1  ! =  L2 . 
caminho ( X ,  Y )  :-  arco ( X ,  Y ,  _ ). 
caminho ( X ,  Z)  :-  arco ( X ,  Y ,  _ ),  caminho ( Y ,  Z ). 
:-  caminho ( X ,  X ). 
:-  raiz ( X ),  ( Y ,  _ ),  X  ! =  Y ,  não  caminho ( X ,  Y ). 
folha ( X )  :-  ( X ,  _ ),  não arco ( X ,  _ ,  _ ).

Padronização de linguagem e competição ASP

O grupo de trabalho de padronização ASP produziu uma especificação de linguagem padrão, chamada ASP-Core-2, [14] para a qual os sistemas ASP recentes estão convergindo. ASP-Core-2 é a linguagem de referência para a Competição de Programação de Conjuntos de Respostas, na qual os solucionadores ASP são periodicamente avaliados em vários problemas de referência.

Comparação de implementações

Os primeiros sistemas, como o Smodels, usavam backtracking para encontrar soluções. À medida que a teoria e a prática dos solucionadores SAT booleanos evoluíram, vários solucionadores ASP foram construídos sobre os solucionadores SAT, incluindo ASSAT e Cmodels. Esses converteram a fórmula ASP em proposições SAT, aplicaram o solucionador SAT e, em seguida, converteram as soluções de volta para o formato ASP. Sistemas mais recentes, como o Clasp, usam uma abordagem híbrida, usando algoritmos orientados a conflitos inspirados no SAT, sem conversão completa em uma forma lógica booleana. Essas abordagens permitem melhorias significativas de desempenho, geralmente em uma ordem de magnitude, em relação aos algoritmos de retrocesso anteriores.

O projeto Potassco atua como um guarda-chuva para muitos dos sistemas abaixo, incluindo clasp , sistemas de aterramento ( gringo ), sistemas incrementais ( iclingo ), solucionadores de restrições ( clingcon ), linguagem de ação para compiladores ASP ( coala ), implementações de MPI distribuídas ( claspar ) , e muitos outros.

A maioria dos sistemas suporta variáveis, mas apenas indiretamente, forçando o aterramento, usando um sistema de aterramento como Lparse ou gringo como front-end. A necessidade de aterramento pode causar uma explosão combinatória de cláusulas; assim, os sistemas que executam o aterramento em tempo real podem ter uma vantagem. [15]

Implementações orientadas a consultas de programação de conjuntos de respostas, como o sistema Galliwasp, [16] s(ASP) [17] e s(CASP) [18] evitam o aterramento usando uma combinação de resolução e coindução .

Plataforma Recursos Mecânica
Nome SO Licença Variáveis Símbolos de função Conjuntos explícitos Listas explícitas Suporte disjuntivo (regras de escolha)
ASPeRiX Linux GPL sim Não aterramento em tempo real
ASSAT Solaris freeware Baseado em solucionador SAT
Solucionador de conjunto de respostas do fecho Linux , macOS , Windows Licença MIT Sim, em Clingo sim Não Não sim incremental, inspirado em solucionador de SAT (nogood, orientado a conflitos)
Cmodels Linux , Solaris GPL Requer aterramento sim incremental, inspirado em solucionador de SAT (nogood, orientado a conflitos)
diff-SAT Linux , macOS , Windows ( máquina virtual Java ) Licença MIT Requer aterramento sim Inspirado no solucionador de SAT (nogood, orientado a conflitos). Suporta a resolução de problemas probabilísticos e amostragem de conjuntos de respostas
DLV Linux , macOS , Windows [19] gratuito para uso educacional acadêmico e não comercial e para organizações sem fins lucrativos [19] sim sim Não Não sim não compatível com Lparse
Complexo DLV Linux , macOS , Windows GPL sim sim sim sim construído em cima de DLV - não compatível com Lparse
GnT Linux GPL Requer aterramento sim construído em cima de smodels
não mais++ Linux GPL combinado literal+baseado em regras
Ornitorrinco Linux , Solaris , Windows GPL distribuído, multi-thread nomore++, smodels
Modelos Pb Linux ? baseado em solucionador pseudo-booleano
Smodels Linux , macOS , Windows GPL Requer aterramento Não Não Não Não
Smodels-cc Linux ? Requer aterramento baseado em solucionador SAT; modelos com cláusulas de conflito
E aí Linux ? Baseado em solucionador SAT

Veja também

Referências

  1. ^ Baral, Chitta (2003). Representação do Conhecimento, Raciocínio e Resolução Declarativa de Problemas . Cambridge University Press. ISBN 978-0-521-81802-5.
  2. ^ Gelfond, Michael (2008). "Conjuntos de respostas" . Em van Harmelen, Frank; Lifschitz, Vladimir; Porter, Bruce (ed.). Manual de Representação do Conhecimento . Elsevier. págs. 285–316. ISBN 978-0-08-055702-1. como PDF Arquivado em 2016-03-03 na Wayback Machine
  3. ^ Dimopoulos, Y.; Nebel, B .; Köhler, J. (1997). "Problemas de planejamento de codificação em programas lógicos não monotônicos". Em Aço, Sam; Alami, Rachid (eds.). Recent Advances in AI Planning: 4th European Conference on Planning, ECP'97, Toulouse, França, 24-26 de setembro de 1997, Proceedings . Notas de aula em Ciência da Computação: Notas de aula em Inteligência Artificial. Vol. 1348. Springer. pp. 273-285. ISBN  978-3-540-63912-1. como pós-escrito
  4. ^ Subrahmanian, VS; Zaniolo, C. (1995). "Relacionando modelos estáveis ​​e domínios de planejamento de IA" . Em Sterling, Leon (ed.). Programação em Lógica: Anais da Décima Segunda Conferência Internacional de Programação em Lógica . Imprensa do MIT. pp. 233-247. ISBN  978-0-262-69177-2. como pós-escrito
  5. ^ Soininen, T.; Niemelä, I. (1998), Formalização do conhecimento de configuração usando regras com escolhas (Postscript) , Laboratório de Ciência do Processamento de Informação, Universidade de Tecnologia de Helsinki
  6. ^ Marek, V.; Truszczyński, M. (1999). "Modelos estáveis ​​e um paradigma de programação lógica alternativa". Em Apt, Krzysztof R. (ed.). O paradigma de programação lógica: uma perspectiva de 25 anos (PDF) . Springer. págs. 169-181. arXiv : cs/9809032 . ISBN  978-3-540-65463-6.
  7. ^ Niemelä, I. (1999). "Programas lógicos com semântica de modelo estável como paradigma de programação de restrição" (Postscript,gzipped) . Anais de Matemática e Inteligência Artificial . 25 (3/4): 241–273. doi : 10.1023/A:1018930122475 .
  8. ^ Lifschitz, V. (1999). "Linguagens de ação, conjuntos de respostas e planejamento". {{cite journal}}:Cite journal requer |journal=( ajuda )Em Apt de 1999 , pp. 357-374
  9. ^ Crick, Tom (2009). Superotimização: Geração de código comprovadamente ótima usando programação de conjunto de respostas (PDF) (Ph.D.). Universidade de Banho. Docket 20352. Arquivado a partir do original (PDF) em 2016-03-04 . Recuperado em 27/05/2011 .
  10. ^ Rogério Dávila. "AnsProlog, uma visão geral" (PowerPoint) .
  11. ^ Niemela, I.; Simons, P.; Soinenen, T. (2000). "Semântica de modelo estável de regras de restrição de peso" . Em Gelfond, Michael; Leone, Nicole; Pfeifer, Gerald (eds.). Programação Lógica e Raciocínio Não-Monotônico: 5ª Conferência Internacional, LPNMR '99, El Paso, Texas, EUA, Anais de 2 a 4 de dezembro de 1999 . Notas de aula em Ciência da Computação: Notas de aula em Inteligência Artificial. Vol. 1730. Springer. págs. 317–331. ISBN 978-3-540-66749-0. como pós-escrito
  12. ^ Ferraris, P.; Lifschitz, V. (janeiro de 2005). "Restrições de peso como expressões aninhadas". Teoria e Prática da Programação em Lógica . 5 (1–2): 45–74. arXiv : cs/0312045 . doi : 10.1017/S1471068403001923 . como pós-escrito
  13. ^ "Análise de dependência" . Arquivado a partir do original em 2015-04-15 . Recuperado 2015-04-15 .
  14. ^ "ASP-Core-2 Input Language Specification" (PDF) . Recuperado em 14 de maio de 2018 .
  15. ^ Lefèvre, Claire; Beatriz, Christopher; Stephan, Igor; Garcia, Laurent (maio de 2017). "ASPeRiX, uma abordagem de encadeamento direto de primeira ordem para computação de conjunto de respostas*" . Teoria e Prática da Programação em Lógica . 17 (3): 266–310. doi : 10.1017/S1471068416000569 . ISSN 1471-0684 . 
  16. ^ Marple, Kyle.; Gupta, Gopal. (2012). "Galliwasp: Um Solucionador de Conjuntos de Respostas Orientados a Objetivos". Em Albert, Elvira (ed.). Síntese e Transformação de Programas Baseados em Lógica, 22º Simpósio Internacional, LOPSTR 2012, Leuven, Bélgica, 18 a 20 de setembro de 2012, Artigos Selecionados Revisados . Springer. pp. 122-136.
  17. ^ Marple, K.; Salazar, E.; Gupta, G. (2017). "Computação de modelos estáveis ​​de programas de lógica normal sem aterramento". CoRR . abs/1709.00501. [1]
  18. ^ Árias, J.; Carro, M.; Salazar, E.; Marple, K.; Gupta, G. (2018). "Programação de conjunto de resposta de restrição sem aterramento". Teoria e Prática da Programação em Lógica . 18 (3–4): 337–354.
  19. ^ a b "Página da empresa do sistema DLV" . DLVSYSTEM srl . Recuperado em 16 de novembro de 2011 .

Links externos