Programação de Conjunto de resposta

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

Programação de Conjunto de Resposta (ASP, da expressão em inglês Answer set programming) é uma forma de programação declarativa orientada a problemas de busca difíceis (principalmente NP-difícil). É baseado na semântica de modelo estável (conjunto de resposta) da programação em lógica. Em ASP, problemas de busca são reduzidos a modelos estáticos de computação, e solucionadores de conjunto de respostas - programas que geram modelos estáveis - são usados para realizar a busca. O processo computacional empregado no design de muitos solucionadores de conjuntos de respostas é uma melhora no algoritmo DPLL e, em princípio, sempre termina (diferentemente do processo de avaliação de consulta Prolog, que pode terminar em um laço infinito).

Em um sentido mais geral, ASP inclui aplicações de conjunto de respostas para representação de conhecimento[1] [2] e o uso da avaliação de consultas no estilo Prolog para resolver problemas decorrentes das aplicações.

História[editar | editar código-fonte]

O método de planejamento automatizado proposto por Dimopoulos, Nebel and Köhler[3] é um exemplo inicial de programação de conjunto de resposta.[quando?] A abordagem deles é baseada no relacionamento entre planos e modelos estáveis.[4] Soininen e Niemelä[5] aplicação o que hoje é chamado de programação de conjunto de resposta para o problema de configuração de produto. O uso de resolvedor de conjunto de repostas para busca foi identificado como um novo paradigma por Marek e Truszczynski em um artigo publicado na perspectiva de 25 anos no paradigma de lógica de programação, publicada em 1999[6] e em [Niemela 1999].[7] A terminologia "conjunto de respostas" ao invés de "modelo estável" foi proposta primeiro por Lifschitz[8] em um artigo publicado no mesmo volume contendo a retrospectiva onde saiu o artigo de Marek-Truszczynski.

Linguagem AnsProlog[editar | editar código-fonte]

Lparse é o nome do programa que foi originalmente criado como uma ferramenta de encalhe (front-end) para o resolvedor de conjunto de resposta smodels. A linguagem que Lparse aceita é hoje chamada de AnsProlog*,[9] pequeno para Resposta para programação de conjunto de respostas em lógica.[10] Ela é hoje usada do mesmo jeito em outros resolvedores de conjunto de respostas, incluindo assat, clasp, cmodels, gNt, nomore++ and pbmodels. (dlv é uma exceção: a sintaxe da ASP ascritos para dlv é um pouco diferente.)

Um programa AnsProlog consiste nas regras da forma:

<head> :- <body> .

O símbolo :- ("if") é derrubado if <body> is empty; essas regras são chamadas de fatos. O jeito simples das regras de Lparse são regras com restrições. Um outro jeito usável construído incluído nesta linguagem é choice. Por exemplo, a regra choice

{p,q,r}.

diz: escolha arbitrariamente qual dos átomos p,q,r incluir no modelo estável. A programação Lparse que contém essa regra "choice" e não tem outras regras, tem 8 modelos estáveis—subconjuntos arbitrários de \{p,q,r\}. A definição de um modelo estável foi generalizada para programas com as regras de choice.[11] A regras de choice também podem ser tratadas como abreviações para fórmulas proposicionais sob o modelo estático de semântica.[12] Por exemplo, o regra da "choice" pode ser vista como um atalho para as fórmulas do conjunto de três "Lei do terceiro excluído":

(p\lor\neg p)\land(q\lor\neg q)\land(r\lor\neg r).

A linguagem de Lparse nos permite escrever "limitadas" regras da Choice, como:

1{p,q,r}2.

A regra diz: escolha no mínimo 1 dos átomos p, q, r, mas não mais que dois. O sentido dessa regra sob a semântica do modelo estável é representado pela fórmula proposicional.

(p\lor\neg p)\land(q\lor\neg q)\land(r\lor\neg r)
\land\,(p\lor q\lor r)\land\neg(p\land q\land r).

Limites de cardinalidade podem ser usados no corpo das regras:

:- 2{p,q,r}.

Adicionando isso a um programa Lparse elimina a semântica de modelo estável que contém ao menos 2 átomos de p,q,r. O significado dessa regra pode ser representado como pela fórmula:

\neg((p\land q)\lor(p\land r)\lor(q\land r)).

Variáveis (capitalizadas como em um Prolog) são usadas em Lparse apra abreviar coleões de regras que seguem o mesmo padrão, e também abreviam coleções de átomos dentro da mesma regra. Por exemplo, o programa Lparse:

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

tem o mesmo significado de:

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

O programa

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

é um atalho para

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

Generalizando modelos estáveis[editar | editar código-fonte]

Para achar um modleo estável de um programa Lparse armazenado na pasta <filename> nós usamos o comando:

% lparse <filename> | smodels

Opção 0 instrui smodels a achar todos os modelos do programa. Por exemplo, se a pasta test contém as regras

1{p,q,r}2.
s :- not p.

então o comando

% lparse test | smodels 0

gera a saída:

Answer: 1
Stable Model: q p 
Answer: 2
Stable Model: p 
Answer: 3
Stable Model: r p 
Answer: 4
Stable Model: q s 
Answer: 5
Stable Model: r s 
Answer: 6
Stable Model: r q s

Exemplo de programas ASP[editar | editar código-fonte]

Coloração de grafo[editar | editar código-fonte]

O coloração de grafos G é uma função color do conjunto de vértices \{1,\dots,n\} de forma que color(x)\neq color(y) para todo par adjacente de vertices x,y. Nós gostaríamos de usar ASP para achar um n-coloração de um grafo (ou determinar que ele não existe).

Isso pode ser realizado usando um programa de Lparse:

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

A linha 1 define os números 1,\dots,n para serem coloridos. De acordo com a regra choice na linha 2, a única cor i deve ser atribuída a cada vértice x. A restrição na linha 3 proíbe pintar a mesma cor de vértices x e y se existe uma conexão entre eles. Se nós combinarmos essa parta com a definição de G:

v(1..100). % 1,...,100 are vertices
e(1,55). % there is an edge from 1 to 55
. . .

e executar smodels sobre ele, com o valor numérico de n especificado na linha de comando, depois os átomos em forma color(\dots,\dots) de saída do smodels irá representar uma n -coloração-de G.

O programa nesse exemplo ilustra a organização "gere-e-teste" que é frequentemente encontrada nos programas simples de ASP. A regra choice descreve o conjunto de "possíveis soluções" - um simples subconjunto do conjunto de soluções para um determinado problema de pesquisa. É seguido pela restrição, que elimita possíveis soluções que não são aceitas. No entando, o processo de pesquisa realizado pelo smodels e outros resolvedores dos conjuntos de respostas, não são baseados no trial and error (tente e erre).

Grande clique[editar | editar código-fonte]

O clique em um grafo é um subconjunto de seus vértices adjacentes. O seguinte programa Lparse encontra um clique de tamanho \geq n no dado grafo, ou determina que não existe.

n {in(X) : v(X)}.
:- in(X), in(Y), v(X), v(Y), X!=Y, not e(X,Y), not e(Y,X).

Existe outro exemplo da organização gere-e-teste. A regra da choice na linha 1 "gera" todos os conjuntos que contém \geq n vértices. A restrição na linha 2 "elimina" os conjuntos que não são cliques.

Caminho Hamiltoniano[editar | editar código-fonte]

O caminho Hamiltoniano em um grafo orientado é um caminho que permite passar através cada vértice do grafo somente uma vez, não repetindo nenhum vértice. O seguinte programa Lparse pode ser usado para achar o caminho Hamiltoniano em um grafo direcionado se ele existe. (Nós assumimos que 0 é um dos vértices)

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

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

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

:- not r(X), v(X).

A regra choice na linha 1 "gera" todos os subconjuntos do conjunto de arestas. As 3 restrições "weed out" do subconjunto não são caminhos hamiltonianos. A última deles usa um predicado auxiliar r(x) ("x é acessível a partir de 0") para proibir os vértices que não satisfazem a condição. Esse predicado é definido recursivamente nas linhas 4 e 5. Esse programa é um exemplo mais geral da "gere, defina e teste"organização: esse inclui a definição de um predicado auxiliar que nos ajuda a eliminar todos as "ruins" potenciais soluções.

Comparação das implementações[editar | editar código-fonte]

Os primeiros sistemas, como Smodels, usavam backtracking(retrocesso) para achar soluções. Como a teoria e prática do problema da satisfatibilidade ooleana, o número de resolvedores ASP foram construídos no topo dos resolvedores SATA, incluindo ASSAT e Cmodels. Essa fórmula ASP convertida em preposições SAT, aplicou o resolvedor SAT,e depois converte a solução de volta para a forma ASP. Sistemas mais recentes, como Clasp, usam uma abordagem híbrida, usando o algoritmo conflict-driven inspirado por SAT, sem a total conversão em uma forma lógica booleana. Essas aproximações permitem melhoras de performance, muitas vezes por ordem de magnetude, em relação a algoritmos de backtracking (algoritmo de retrocesso).

O projeto Potassco age como um guarda-chuva para vários sistemas abaixo, incluindo clasp, sistemas de aterramento (gringo), sistemas incrementais (iclingo), resolvedores de restrição (cligcon), linguagem de ação para ASP copiladores (coala), implementação distribuída MPI (claspar), e outros.

A maioria dos sistemas suportam variáveis, mas apenas indiretamente, forçando o aterramento, usando o sistema de aterramento como um Lparse ou gringo como front-end. A necessidade de aterramento pode causar a explosão de uma combinação de cláusulas, assim, sistemas que executam aterramento on-the-fly podem ter uma vantagem.

Plataforma Características Mecânica
Nome OS Licença Variáveis Símbolos de função Conjuntos explícitos Listas explícitas Apoio (regras da choice) dijuntivo
ASPeRiX Linux GPL Sim Não on-the-fly grounding
ASSAT Solaris Freeware SAT-solver based
Clasp Answer Set Solver Linux, Mac OS, Windows GPL Yes, in Clingo yes no no Yes, in ClaspD incremental, SAT-solver inspired (nogood, conflict-driven)
Cmodels Linux, Solaris GPL Predefinição:Okay Sim incremental, SAT-solver inspired (nogood, conflict-driven)
DLV Linux, Mac OS, Windows[13] free for academic and non-commercial educational use, and for non-profit organizations[13] Sim Sim Não Não Sim Não é compatível em Lparse
DLV-Complex Linux, Mac OS, Windows Freeware Sim Sim Sim Sim built on top of DLV — not Lparse compatible
GnT Linux GPL Predefinição:Okay Sim built on top of smodels
nomore++ Linux GPL combined literal+rule-based
Platypus Linux, Solaris, Windows GPL distributed, multi-threaded nomore++, smodels
Pbmodels Linux ? pseudo-boolean solver based
Smodels Linux, Mac OS, Windows GPL Predefinição:Okay Não Não Não Não
Smodels-cc Linux ? Predefinição:Okay SAT-solver based; smodels w/conflict clauses
Sup Linux ? SAT-solver based

Veja também[editar | editar código-fonte]

Referências

  1. Baral, Chitta. Knowledge Representation, Reasoning and Declarative Problem Solving. [S.l.]: Cambridge University Press, 2003. ISBN 978-0-521-81802-5
  2. Gelfond, Michael. Handbook of Knowledge Representation. [S.l.]: Elsevier, 2008. 285–316 pp. ISBN 978-0-08-055702-1 as PDF
  3. Dimopoulos, Y.; Nebel, B.; Köhler, J.. In: Y.. Recent Advances in AI Planning: 4th European Conference on Planning, ECP'97, Toulouse, France, September 24–26, 1997, Proceedings. [S.l.]: Springer, 1997. 273–285 pp. vol. 1348. ISBN 978-3-540-63912-1 as Postscript
  4. Subrahmanian, V.S.; Zaniolo, C.. In: V.S.. Logic Programming: Proceedings of the Twelfth International Conference on Logic Programming. [S.l.]: MIT Press, 1995. 233–247 pp. ISBN 978-0-262-69177-2 as Postscript
  5. Predefinição:Cite techreport
  6. Marek, V.; Truszczyński, M.. In: V.. The Logic programming paradigm: a 25-year perspective. [S.l.]: Springer, 1999. 169–181 pp. ISBN 978-3-540-65463-6
  7. Niemelä, I.. (1999). "Logic programs with stable model semantics as a constraint programming paradigm" (Postscript). Annals of Mathematics and Artificial Intelligence 25: 241–273 pp.. DOI:10.1023/A:1018930122475.
  8. "". In Apt 1999, pp. 357–374
  9. .. , .
  10. Rogelio Davila. AnsProlog, an overview (PowerPoint).
  11. Niemelä, I.; Simons, P.; Soinenen, T.. In: I.. Logic Programming and Nonmonotonic Reasoning: 5th International Conference, LPNMR '99, El Paso, Texas, USA, December 2–4, 1999 Proceedings. [S.l.]: Springer, 2000. 317–331 pp. vol. 1730. ISBN 978-3-540-66749-0 as Postscript
  12. (January 2005) "Weight constraints as nested expressions" (PDF). Theory and Practice of Logic Programming 5 (1-2): 45–74 pp.. DOI:10.1017/S1471068403001923. as Postscript
  13. a b DLV System company page. DLVSYSTEM s.r.l.. Página visitada em 16 November 2011.

Ligações externas[editar | editar código-fonte]