# Programação de conjunto de resposta

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 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 é um exemplo inicial de programação de conjunto de resposta. A abordagem deles é baseada no relacionamento entre planos e modelos estáveis. Soininen e Niemelä 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 e em [Niemela 1999]. A terminologia "conjunto de respostas" ao invés de "modelo estável" foi proposta primeiro por Lifschitz em um artigo publicado no mesmo volume contendo a retrospectiva onde saiu o artigo de Marek-Truszczynski.

## Linguagem AnsProlog

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*, pequeno para Resposta para programação de conjunto de respostas em lógica. 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:
O símbolo :- ("if") não é usado caso o conteúdo de <body> 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
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. A regras de choice também podem ser tratadas como abreviações para fórmulas proposicionais sob o modelo estático de semântica. 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:
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:
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:
tem o mesmo significado de:
O programa
é um atalho para

## Generalizando modelos estáveis

Para achar um modelo estável de um programa Lparse armazenado na pasta <filename> nós usamos o comando:
Opção 0 instrui smodels a achar todos os modelos do programa. Por exemplo, se a pasta test contém as regras
então o comando
gera a saída:

## Exemplo de programas ASP
### Coloração de grafo

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:
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$:
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 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 $\geq n$ no dado grafo, ou determina que não existe.
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

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)
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

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 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 | Plataforma | Plataforma | Características | Características | Características | Características | 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 | free for academic and non-commercial educational use, and for non-profit organizations | 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

* Programação lógica
* Lógica não-monotônica
* Prolog
* Satisfação de restrições