Programação por conjuntos
2010/2011
Relatório Trabalho Prático 3 – Turno P4
Utilização da programação por conjuntos de resposta SMODELS na resolução de problemas combinatórios.
[Página deixada em branco intencionalmente]
Introdução
Neste trabalho pretende-se utilizar o paradigma de programação por conjuntos de resposta (answer-set programming), recorrendo ao programa SMODELS, que implementa a semântica dos modelos estáveis para programas em lógica, que no nosso caso de estudo, passa por modelar um problema combinatório. Em conjunto com o smodels vamos utilizar o programa lparse que adiciona variáveis à linguagem que se está a escrever, gerando assim um programa em lógica, livre de variáveis para que o smodels o possa processar. O lparse para além da semântica de modelo estável, implementa também a semântica da negação clássica e a de modelos estáveis parciais entre outros, fazendo depois a tradução para programas de lógica normal. Na semântica dos modelos estáveis, os modelos são validados pelo programa ou seja só podemos ter coisas verdadeiras para as quais tenho um antecedente com uma regra verdadeira. Os modelos podem ser vistos como cenários possíveis, podendo cada programa ter nenhum, um ou vários modelos estáveis. Para determinar um modelos estável, é utilizada a transformação de Gelfond-Lifschitz, em que um modelo é estável se e só se: I = least (P/I), sendo I uma interpretação (conjunto de átomos), e least(P/I) um programa positivo, que por definição tem apenas um único modelo mínimo.
A programação por conjuntos de resposta aparece então com a expressividade da programação em lógica com a semântica dos modelos estáveis. Os conjuntos de resposta ou modelos estáveis correspondem a uma solução. Este paradigma de semântica de modelo estável garante a completude, ou seja, a descoberta de uma solução é garantida.
Desenvolvimento
O problema a modelar, tem por base a análise das observações recolhidas por um Rover em Marte em cinco