Mostrar código-fonte de Programação de conjunto de resposta

{{Reciclagem|data=agosto de 2023}}
'''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]]<ref>{{citar livro|primeiro =Chitta |último =Baral |título=Knowledge Representation, Reasoning and Declarative Problem Solving |url=http://books.google.com/books?id=iTS4ZdEpGZQC |ano=2003 |publicado=Cambridge University Press |isbn=978-0-521-81802-5}}</ref><ref>{{citar livro |primeiro =Michael |último =Gelfond |capítulo =Answer sets |editor-nome1 =Frank |editor-sobrenome1 =van Harmelen |editor-nome2 =Vladimir |editor-sobrenome2 =Lifschitz |editor-nome3 =Bruce |editor-sobrenome3 =Porter |título =Handbook of Knowledge Representation |url =http://books.google.com/books?id=xwBDylHhJhYC&pg=PA285 |ano =2008 |publicado =Elsevier |isbn =978-0-08-055702-1 |páginas =285–316 }} [http://www.depts.ttu.edu/cs/research/krlab/pdfs/papers/gel07b.pdf as PDF] {{Wayback|url=http://www.depts.ttu.edu/cs/research/krlab/pdfs/papers/gel07b.pdf |date=20160303231241 }}</ref> e o uso da avaliação de consultas no estilo Prolog para resolver problemas decorrentes das aplicações.

==História==

O método de [[planejamento automatizado]] proposto por Dimopoulos, Nebel and Köhler<ref>{{citar livro|primeiro1 =Y. |último1 =Dimopoulos |autorlink2 =Bernhard Nebel |primeiro2 =B. |último2 =Nebel |primeiro3 =J. |último3 =Köhler |capítulo=Encoding planning problems in non-monotonic logic programs |páginas=273–285 |editor-nome1 =Sam |editor-sobrenome1 =Steel |editor-nome2 =Rachid |editor-sobrenome2 =Alami |título=Recent Advances in AI Planning: 4th European Conference on Planning, ECP'97, Toulouse, France, September 24–26, 1997, Proceedings |url=http://books.google.com/books?id=QSBoQgAACAAJ |ano=1997 |publicado=Springer |isbn=978-3-540-63912-1 |volume=1348 |series=Lecture notes in computer science: Lecture notes in artificial intelligence}} [ftp://ftp.informatik.uni-freiburg.de/documents/papers/ki/dimopoulos-etal-ecp97.ps.gz as Postscript]</ref> é um exemplo inicial de programação de conjunto de resposta. A abordagem deles é baseada no relacionamento entre planos e modelos estáveis.<ref>{{citar livro|primeiro1 =V.S. |último1 =Subrahmanian |primeiro2 =C. |último2 =Zaniolo |capítulo=Relating stable models and AI planning domains |editor-nome =Leon |editor-sobrenome =Sterling |título=Logic Programming: Proceedings of the Twelfth International Conference on Logic Programming |capítulourl=http://books.google.com/books?id=vpGEyZWP1dYC&pg=PA233 |ano=1995 |publicado=MIT Press |isbn=978-0-262-69177-2 |páginas=233–247}} [http://www.cs.ucla.edu/%7Ezaniolo/papers/iclp95.ps as Postscript]</ref> Soininen e Niemelä<ref>{{citar periódico|último=Soininen|primeiro=T|coautores=Niemelä I.|título=Formalizing configuration knowledge using rules with choices|ano=1998|número=TKO-B142|url=http://www.tcs.hut.fi/~ini/papers/sn-faanmr98.ps.gz|local=institution=Laboratory of Information Processing Science, Helsinki University of Technology}}</ref> 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<ref>{{citar livro|primeiro1 =V. |último1 =Marek |primeiro2 =M. |último2 =Truszczyński |capítulo=Stable models and an alternative logic programming paradigm |editor-nome =Krzysztof R. |editor-sobrenome =Apt |título=The Logic programming paradigm: a 25-year perspective |url=http://books.google.com/books?id=GIhQAAAAMAAJ |ano=1999 |publicado=Springer |isbn=978-3-540-65463-6 |capítulourl=http://xxx.lanl.gov/pdf/cs/9809032 |formato=PDF |páginas=169–181 |ref={{harvid|Apt|1999}}}}</ref>  e em [Niemela 1999].<ref>{{citar periódico|primeiro =I. |último =Niemelä |título=Logic programs with stable model semantics as a constraint programming paradigm |periódico=Annals of Mathematics and Artificial Intelligence |volume=25 |páginas=241–273 |ano=1999 |doi=10.1023/A:1018930122475 |url=http://www.tcs.hut.fi/~ini/papers/lp-csp-long.ps |formato=Postscript}}</ref>   A terminologia "conjunto de respostas" ao invés de "modelo estável" foi proposta primeiro por Lifschitz<ref>{{citar periódico|primeiro =V. |último =Lifschitz |título=Action Languages, Answer Sets, and Planning |ano=1999}} In {{harvnb|Apt|1999|pp=357–374}}</ref> em um artigo publicado no mesmo volume contendo a retrospectiva onde saiu o artigo de Marek-Truszczynski.

==Linguagem AnsProlog==

[http://www.tcs.hut.fi/Software/smodels/lparse.ps Lparse] é o nome do programa que foi originalmente criado como uma ferramenta de encalhe (front-end) para o resolvedor de conjunto de resposta [http://www.tcs.hut.fi/Software/smodels/ smodels]. A linguagem que Lparse aceita é hoje chamada de AnsProlog*,<ref>{{citar tese|tipo=Ph.D. |título=Superoptimisation: Provably Optimal Code Generation using Answer Set Programming |url=http://opus.bath.ac.uk/20352/1/UnivBath_PhD_2009_T_Crick.pdf |último =Crick |primeiro =Tom |ano=2009 |publicado=University of Bath |docket=20352 }}</ref> pequeno para ''Resposta para programação de conjunto de respostas em lógica''.<ref>{{citar web|autor =Rogelio Davila |título=AnsProlog, an overview |url=http://www.rogeliodavila.com/Programacion%20Logica/PL%20Notas/AnsProlog%20Overview.ppt |formato=PowerPoint}}</ref> Ela é hoje usada do mesmo jeito em outros resolvedores de conjunto de respostas, incluindo [http://assat.cs.ust.hk/ assat], [http://www.cs.uni-potsdam.de/clasp/ clasp], [http://www.cs.utexas.edu/users/tag/cmodels/ cmodels], [http://www.tcs.hut.fi/Software/gnt/ gNt], [http://www.cs.uni-potsdam.de/nomore/ nomore++] and [http://www.cs.uky.edu/ai/pbmodels/ pbmodels]. ([http://www.dbai.tuwien.ac.at/proj/dlv/ dlv] é uma exceção: a sintaxe da ASP ascritos para dlv é um pouco diferente.)

Um programa AnsProlog  consiste nas regras da forma:

<pre>
<head> :- <body> .
</pre>

O símbolo <code>:-</code> ("if") não é usado caso o conteúdo de <code><body></code> esteja vazio. 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''

<pre>
{p,q,r}.
</pre>

diz: escolha arbitrariamente qual dos átomos <math>p,q,r</math> 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 <math>\{p,q,r\}</math>. A definição de um modelo estável foi generalizada para programas com as regras de choice.<ref>{{citar livro|primeiro1 =I. |último1 =Niemelä |primeiro2 =P. |último2 =Simons |primeiro3 =T. |último3 =Soinenen |capítulo=Stable model semantics of weight constraint rules |editor-nome1 =Michael |editor-sobrenome1 =Gelfond |editor-nome2 =Nicole |editor-sobrenome2 =Leone |editor-nome3 =Gerald |editor-sobrenome3 =Pfeifer |título=Logic Programming and Nonmonotonic Reasoning: 5th International Conference, LPNMR '99, El Paso, Texas, USA, December 2–4, 1999 Proceedings |capítulourl=http://books.google.com/books?id=Abj-OpFeDjQC&pg=PA317 |ano=2000 |publicado=Springer |isbn=978-3-540-66749-0 |páginas=317–331 |series=Lecture notes in computer science: Lecture notes in artificial intelligence |volume=1730}} [http://www.tcs.hut.fi/~ini/papers/nss-lpnmr99-www.ps.gz as Postscript]</ref> A regras de choice também podem ser tratadas como abreviações para fórmulas proposicionais sob o modelo estático de semântica.<ref>{{citar periódico|primeiro1 =P. |último1 =Ferraris |primeiro2 =V. |último2 =Lifschitz |título=Weight constraints as nested expressions |periódico=Theory and Practice of Logic Programming |volume=5 |número=1-2 |páginas=45–74 |data=janeiro de 2005 |doi=10.1017/S1471068403001923 |url=http://arxiv.org/pdf/cs/0312045 |formato=PDF}} [http://www.cs.utexas.edu/users/vl/papers/weight.ps as Postscript]</ref>  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]]":

:<math>(p\lor\neg p)\land(q\lor\neg q)\land(r\lor\neg r).</math>

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

<pre>
1{p,q,r}2.
</pre>

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.

:<math>(p\lor\neg p)\land(q\lor\neg q)\land(r\lor\neg r)</math>

::<math>\land\,(p\lor q\lor r)\land\neg(p\land q\land r).</math>

Limites de cardinalidade podem ser usados no corpo das regras:

<pre>
:- 2{p,q,r}.
</pre>

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

::<math>\neg((p\land q)\lor(p\land r)\lor(q\land r)).</math>

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:

<pre>
p(a). p(b). p(c).
q(X) :- p(X), X!=a.
</pre>

tem o mesmo significado de:

<pre>
p(a). p(b). p(c).
q(b). q(c).
</pre>

O programa

<pre>
p(a). p(b). p(c).
{q(X):p(X)}2.
</pre>

é um atalho para

<pre>
p(a). p(b). p(c).
{q(a),q(b),q(c)}2.
</pre>

==Generalizando modelos estáveis==

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

<pre>
% lparse <filename> | smodels
</pre>

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

<pre>
1{p,q,r}2.
s :- not p.
</pre>

então o comando

<pre>
% lparse test | smodels 0
</pre>

gera a saída:

<pre>
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
</pre>

==Exemplo de programas ASP==

===Coloração de grafo===

O [[coloração de grafos]] G é uma função color do conjunto de vértices <math>\{1,\dots,n\}</math> de forma que <math>color(x)\neq color(y)</math> para todo par adjacente de vertices <math>x,y</math>. 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:

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

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

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

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

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 limita possíveis soluções que não são aceitas. No entanto, 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==

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

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

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

==Caminho Hamiltoniano==

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)

<pre>
{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).
</pre>

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 <math>r(x)</math> ("<math>x</math> é 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==

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 magnitude, em relação a algoritmos de backtracking (algoritmo de retrocesso).

O projeto [http://potassco.sourceforge.net/ 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.

{| class="wikitable"
|-
! colspan="3" | Plataforma
! colspan="5" | Características
! colspan="1" | Mecânica
|-
! style="background:#ffdead;" | Nome
! style="background:#ffdead;" | OS
! style="background:#ffdead;" | Licença
! style="background:#ffdead;" | Variáveis
! style="background:#ffdead;" | Símbolos de função
! style="background:#ffdead;" | Conjuntos explícitos
! style="background:#ffdead;" | Listas explícitas
! style="background:#ffdead;" | Apoio (regras da choice) dijuntivo
!
|-
|{{rh}}|[http://www.info.univ-angers.fr/pub/claire/asperix/ ASPeRiX]
|[[Linux]]
|[[GNU General Public License|GPL]]
|Sim
|
|
|
|Não
|on-the-fly grounding
|-
|{{rh}}|[http://assat.cs.ust.hk/ ASSAT]
|[[Solaris (operating system)|Solaris]]
|[[Freeware]]
|
|
|
|
|
|SAT-solver based
|-
|{{rh}}|[http://www.cs.uni-potsdam.de/clasp/ Clasp Answer Set Solver]
|[[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]]
|[[GNU General Public License|GPL]]
|yes|Yes, in Clingo
|yes
|no
|no
|Yes, in ClaspD
|incremental, SAT-solver inspired (nogood, conflict-driven)
|-
|{{rh}}|[http://www.cs.utexas.edu/users/tag/cmodels/ Cmodels]
|[[Linux]], [[Solaris (operating system)|Solaris]]
|[[GNU General Public License|GPL]]
|{{okay|Requires grounding}}
|
|
|
|Sim
|incremental, SAT-solver inspired (nogood, conflict-driven)
|-
|{{rh}}|[[DLV]]
|[[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]]<ref name="dlvsystem.com">{{citar web|url=http://www.dlvsystem.com |título=DLV System company page |publicado=DLVSYSTEM s.r.l. |acessodata=16 de novembro de 2011}}</ref>
|free for academic and non-commercial educational use, and for non-profit organizations<ref name="dlvsystem.com" />
|Sim
|Sim
|Não
|Não
|Sim
|Não é compatível em Lparse
|-
|{{rh}}|[http://www.mat.unical.it/dlv-complex/ DLV-Complex]
|[[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]]
|[[Freeware]]
|
|Sim
|Sim
|Sim
|Sim
|built on top of [[DLV]] — not Lparse compatible
|-
|{{rh}}|[http://www.tcs.hut.fi/Software/gnt/ GnT]
|[[Linux]]
|[[GNU General Public License|GPL]]
|{{okay|Requires grounding}}
|
|
|
|Sim
| built on top of smodels
|-
|{{rh}}|[http://www.cs.uni-potsdam.de/nomore/ nomore++]
|[[Linux]]
|[[GNU General Public License|GPL]]
|
|
|
|
|
|combined literal+rule-based
|-
|{{rh}}|[http://www.cs.uni-potsdam.de/platypus/ Platypus]
|[[Linux]], [[Solaris (operating system)|Solaris]], [[Microsoft Windows|Windows]]
|[[GNU General Public License|GPL]]
|
|
|
|
|
|distributed, multi-threaded nomore++, smodels
|-
|{{rh}}|[http://www.cs.uky.edu/ai/pbmodels/ Pbmodels]
|[[Linux]]
|?
|
|
|
|
|
|[[pseudo-boolean]] solver based
|-
|{{rh}}|[http://www.tcs.hut.fi/Software/smodels/ Smodels]
|[[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]]
|[[GNU General Public License|GPL]]
|{{okay|Requires grounding}}
|Não
|Não
|Não
|Não
|
|-
|{{rh}}|[http://www.nku.edu/~wardj1/Research/smodels_cc.html Smodels-cc]
|[[Linux]]
|?
|{{okay|Requires grounding}}
|
|
|
|
|SAT-solver based; smodels w/conflict clauses
|-
|{{rh}}|[http://www.cs.utexas.edu/users/tag/sup/ Sup]
|[[Linux]]
|?
|
|
|
|
|
|SAT-solver based
|}

==Veja também==
*[[Programação lógica]]
*[[Lógica não-monotônica]]
*[[Prolog]]
*[[Satisfação de restrições]]

{{referências}}

== Ligações externas ==
*[http://asparagus.cs.uni-potsdam.de/contest/ First ASP System Competition]
*[http://www.cs.kuleuven.be/~dtai/events/ASP-competition/index.shtml Second ASP Competition]
*[http://www.mat.unical.it/aspcomp2011/ Third ASP Competition]
*[http://www.mat.unical.it/aspcomp2013 Fourth ASP Competition]
*[http://www.cs.uni-potsdam.de/platypus/ Platypus]
*[http://www.kr.tuwien.ac.at/staff/tkren/deb.html A variety of answer set solvers packaged for Debian / Ubuntu]
*[http://www.cs.uni-potsdam.de/clasp/ Clasp Answer Set Solver]

{{DEFAULTSORT:Programação de Conjunto de Respostas}}
[[Categoria:Programação lógica]]