Programação de lógica de restrição - Constraint logic programming

A programação lógica de restrição é uma forma de programação de restrição , na qual a programação lógica é estendida para incluir conceitos de satisfação de restrição . Um programa lógico de restrição é um programa lógico que contém restrições no corpo das cláusulas. Um exemplo de uma cláusula que inclui uma restrição é . Nesta cláusula, é uma restrição; , E são literais como em lógica de programação regular. Esta cláusula estabelece uma condição sob a qual a declaração é válida: é maior que zero e ambos e são verdadeiros. A(X,Y) :- X+Y>0, B(X), C(Y)X+Y>0A(X,Y)B(X)C(Y)A(X,Y)X+YB(X)C(Y)

Como na programação de lógica regular, os programas são questionados sobre a comprovação de um objetivo, que pode conter restrições além de literais. Uma prova para um objetivo é composta de cláusulas cujos corpos são restrições satisfatórias e literais que, por sua vez, podem ser provados usando outras cláusulas. A execução é realizada por um intérprete, que parte da meta e faz a varredura recursiva das cláusulas tentando comprovar a meta. As restrições encontradas durante esta varredura são colocadas em um conjunto denominado armazenamento de restrições . Se este conjunto for considerado insatisfatório, o intérprete volta atrás , tentando usar outras cláusulas para comprovar o objetivo. Na prática, a satisfatibilidade do armazenamento de restrições pode ser verificada usando um algoritmo incompleto, que nem sempre detecta inconsistência.

Visão geral

Formalmente, os programas de lógica de restrição são como programas de lógica regulares, mas o corpo das cláusulas pode conter restrições, além dos literais de programação de lógica regular. Por exemplo, X>0é uma restrição e está incluída na última cláusula do seguinte programa de lógica de restrição.

B(X,1):- X<0.
B(X,Y):- X=1, Y>0.
A(X,Y):- X>0, B(X,Y).

Como na programação de lógica regular, avaliar um objetivo como A(X,1)requer a avaliação do corpo da última cláusula com Y=1. Como na programação lógica regular, isso, por sua vez, requer a comprovação do objetivo B(X,1). Ao contrário da programação lógica regular, isso também requer que uma restrição seja satisfeita X>0:, a restrição no corpo da última cláusula (na programação lógica regular, X> 0 não pode ser provado a menos que X esteja vinculado a um termo totalmente básico e à execução do o programa irá falhar se esse não for o caso).

Se uma restrição é satisfeita nem sempre pode ser determinado quando a restrição é encontrada. Neste caso, por exemplo, o valor de Xnão é determinado quando a última cláusula é avaliada. Como resultado, a restrição X>0não é satisfeita nem violada neste ponto. Em vez de prosseguir na avaliação de B(X,1)e, em seguida, verificar se o valor resultante de Xé positivo posteriormente, o interpretador armazena a restrição X>0e, em seguida, prossegue na avaliação de B(X,1); dessa forma, o intérprete pode detectar a violação da restrição X>0durante a avaliação de B(X,1)e retroceder imediatamente se for o caso, em vez de esperar que a avaliação de B(X,1)para concluir.

Em geral, a avaliação de um programa de lógica de restrição procede da mesma forma que um programa de lógica regular. No entanto, as restrições encontradas durante a avaliação são colocadas em um conjunto denominado armazenamento de restrições. A título de exemplo, a avaliação do objetivo A(X,1)prossegue avaliando o corpo da primeira cláusula com Y=1; esta avaliação adiciona X>0ao armazenamento de restrição e requer que o objetivo B(X,1)seja comprovado. Ao tentar provar esse objetivo, a primeira cláusula é aplicada, mas sua avaliação adiciona X<0ao armazenamento de restrição. Essa adição torna o armazenamento de restrições insatisfatório. O interpretador então retrocede, removendo a última adição do armazenamento de restrições. A avaliação da segunda cláusula adiciona X=1e Y>0ao armazenamento de restrição. Como o armazenamento de restrições é satisfatório e nenhum outro literal é deixado para provar, o interpretador pára com a solução X=1, Y=1.

Semântica

A semântica dos programas de lógica de restrição pode ser definida em termos de um interpretador virtual que mantém um par durante a execução. O primeiro elemento desse par é chamado de objetivo atual; o segundo elemento é chamado de armazenamento de restrição. O objetivo atual contém os literais que o intérprete está tentando provar e também pode conter algumas restrições que está tentando satisfazer; o armazenamento de restrições contém todas as restrições que o interpretador considerou satisfatórias até agora. ${\ displaystyle \ langle G, S \ rangle}$

Inicialmente, o objetivo atual é o objetivo e o armazenamento de restrições está vazio. O intérprete prossegue removendo o primeiro elemento do objetivo atual e analisando-o. Os detalhes desta análise são explicados abaixo, mas no final, essa análise pode produzir um encerramento bem-sucedido ou uma falha. Essa análise pode envolver chamadas recursivas e adição de novos literais ao objetivo atual e nova restrição ao armazenamento de restrição. O intérprete retrocede se uma falha for gerada. Uma rescisão bem-sucedida é gerada quando a meta atual está vazia e o armazenamento de restrição é satisfatório.

Os detalhes da análise de um literal removido da meta são os seguintes. Depois de remover este literal da frente da meta, é verificado se é uma restrição ou um literal. Se for uma restrição, será adicionado ao armazenamento de restrições. Se for um literal, é escolhida uma cláusula cujo cabeçalho tem o mesmo predicado do literal; a cláusula é reescrita substituindo suas variáveis ​​por novas variáveis ​​(variáveis ​​que não ocorrem na meta): o resultado é chamado de uma nova variante da cláusula; o corpo da nova variante da cláusula é então colocado na frente do gol; a igualdade de cada argumento do literal com o correspondente da nova cabeça variante é colocada na frente do gol também.

Algumas verificações são feitas durante essas operações. Em particular, o armazenamento de restrição é verificado quanto à consistência sempre que uma nova restrição é adicionada a ele. Em princípio, sempre que o armazenamento de restrições for insatisfatório, o algoritmo pode retroceder. No entanto, verificar a insatisfação em cada etapa seria ineficiente. Por esta razão, um verificador de satisfatibilidade incompleto pode ser usado em seu lugar. Na prática, a satisfatibilidade é verificada usando métodos que simplificam o armazenamento de restrições, ou seja, reescrevem em uma forma equivalente, mas mais simples de resolver. Esses métodos podem às vezes, mas nem sempre, provar a insatisfação de um armazenamento de restrição insatisfatório.

O intérprete provou a meta quando a meta atual está vazia e o armazenamento de restrição não é detectado como insatisfatório. O resultado da execução é o conjunto atual de restrições (simplificadas). Este conjunto pode incluir restrições, como aquelas que forçam as variáveis ​​a um valor específico, mas também pode incluir restrições como aquelas que apenas limitam as variáveis ​​sem dar a elas um valor específico. ${\ displaystyle X = 2}$${\ displaystyle X> 2}$

Formalmente, a semântica da programação lógica de restrição é definida em termos de derivações . Uma transição é um par de pares objetivo / loja, observou . Tal par indica a possibilidade de ir de um estado a outro . Essa transição é possível em três casos possíveis: ${\ displaystyle \ langle G, S \ rangle \ rightarrow \ langle G ', S' \ rangle}$${\ displaystyle \ langle G, S \ rangle}$${\ displaystyle \ langle G ', S' \ rangle}$

• um elemento de G é uma restrição C , e ; em outras palavras, uma restrição pode ser movida da meta para o armazenamento de restrição${\ displaystyle G '= G \ barra invertida \ {C \}}$${\ displaystyle S '= S \ xícara \ {C \}}$
• um elemento de G é um literal , existe uma cláusula que, reescrita usando novas variáveis, é , é G com substituído por , e ; em outras palavras, um literal pode ser substituído pelo corpo de uma nova variante de uma cláusula com o mesmo predicado na cabeça, adicionando o corpo da nova variante e as igualdades de termos acima para o objetivo${\ displaystyle L (t_ {1}, \ ldots, t_ {n})}$${\ displaystyle L (t_ {1} ', \ ldots, t_ {n}'): - B}$${\ displaystyle G '}$${\ displaystyle L (t_ {1}, \ ldots, t_ {n})}$${\ displaystyle t_ {1} = t_ {1} ', \ ldots, t_ {n} = t_ {n}', B}$${\ displaystyle S '= S}$
• S e são equivalentes de acordo com a semântica de restrição específica${\ displaystyle S '}$

Uma sequência de transições é uma derivação. Um objetivo G pode ser provado se existe uma derivação de para para alguma restrição S satisfatória . Essa semântica formaliza as possíveis evoluções de um intérprete que escolhe arbitrariamente o literal do objetivo a ser processado e a cláusula para substituir os literais. Em outras palavras, um objetivo é comprovado sob esta semântica se existe uma sequência de escolhas de literais e cláusulas, entre as possivelmente muitas, que conduzem a um objetivo vazio e armazenamento satisfatório. ${\ displaystyle \ langle G, \ emptyset \ rangle}$${\ displaystyle \ langle \ emptyset, S \ rangle}$

Os intérpretes reais processam os elementos da meta em uma ordem LIFO : os elementos são adicionados na frente e processados ​​na frente. Eles também escolhem a cláusula da segunda regra de acordo com a ordem em que foram escritas e reescrevem o armazenamento de restrição quando ele é modificado.

O terceiro tipo possível de transição é a substituição do armazenamento de restrições por um equivalente. Essa substituição é limitada àquelas feitas por métodos específicos, como a propagação de restrição . A semântica da programação lógica de restrição é paramétrica não apenas para o tipo de restrição usada, mas também para o método para reescrever o armazenamento de restrição. Os métodos específicos usados ​​na prática substituem o armazenamento de restrições por um mais simples de resolver. Se o armazenamento de restrição for insatisfatório, essa simplificação pode detectar essa insatisfação algumas vezes, mas nem sempre.

O resultado da avaliação de uma meta em relação a um programa lógico de restrição é definido se a meta for comprovada. Nesse caso, existe uma derivação do par inicial para um par onde a meta é vazia. O armazenamento de restrição deste segundo par é considerado o resultado da avaliação. Isso ocorre porque o armazenamento de restrições contém todas as restrições consideradas satisfatórias para provar o objetivo. Em outras palavras, o objetivo é comprovado para todas as avaliações de variáveis ​​que atendem a essas restrições.

A igualdade de pares de termos de dois literais é freqüentemente denotada de forma compacta por : esta é uma abreviatura para as restrições . Uma variante comum da semântica para programação de lógica de restrição adiciona diretamente ao armazenamento de restrição em vez de ao objetivo. ${\ displaystyle L (t_ {1}, \ ldots, t_ {n}) = L (t_ {1} ', \ ldots, t_ {n}')}$${\ displaystyle t_ {1} = t_ {1} ', \ ldots, t_ {n} = t_ {n}'}$${\ displaystyle L (t_ {1}, \ ldots, t_ {n}) = L (t_ {1} ', \ ldots, t_ {n}')}$

Termos e Condições

Diferentes definições de termos são usadas, gerando diferentes tipos de programação lógica de restrição: sobre árvores, reais ou domínios finitos. Um tipo de restrição sempre presente é a igualdade de termos. Essas restrições são necessárias porque o intérprete adiciona t1=t2ao objetivo sempre que um literal P(...t1...)é substituído pelo corpo de uma nova variante de cláusula cuja cabeça é P(...t2...).

Termos da árvore

A programação lógica de restrição com termos de árvore emula a programação lógica regular, armazenando substituições como restrições no armazenamento de restrição. Os termos são variáveis, constantes e símbolos de função aplicados a outros termos. As únicas restrições consideradas são as igualdades e desigualdades entre os termos. A igualdade é particularmente importante, pois restrições como t1=t2são frequentemente geradas pelo intérprete. As restrições de igualdade nos termos podem ser simplificadas, ou seja, resolvidas por meio da unificação :

Uma restrição t1=t2pode ser simplificada se ambos os termos forem símbolos de função aplicados a outros termos. Se os dois símbolos de função forem iguais e o número de subtermos também for o mesmo, essa restrição pode ser substituída pela igualdade de subtermos aos pares. Se os termos são compostos de diferentes símbolos de função ou do mesmo functor, mas em diferentes números de termos, a restrição é insatisfatória.

Se um dos dois termos for uma variável, o único valor permitido que a variável pode assumir é o outro termo. Como resultado, o outro termo pode substituir a variável na meta e armazenamento de restrição atuais, praticamente removendo a variável de consideração. No caso particular de igualdade de uma variável consigo mesma, a restrição pode ser removida como sempre satisfeita.

Nessa forma de satisfação de restrição, os valores das variáveis ​​são termos.

Reais

A programação lógica de restrição com números reais usa expressões reais como termos. Quando nenhum símbolo de função é usado, os termos são expressões sobre reais, possivelmente incluindo variáveis. Nesse caso, cada variável só pode aceitar um número real como valor.

Para ser mais preciso, os termos são expressões sobre variáveis ​​e constantes reais. A igualdade entre os termos é um tipo de restrição que está sempre presente, pois o intérprete gera igualdade de termos durante a execução. Por exemplo, se o primeiro literal do objetivo atual for A(X+1)e o interpretador tiver escolhido uma cláusula que é A(Y-1):-Y=1após a reescrita de variáveis, as restrições adicionadas ao objetivo atual são X+1=Y-1e . As regras de simplificação usadas para símbolos de função obviamente não são usadas: não é insatisfatório apenas porque a primeira expressão é construída usando e a segunda usando . ${\ displaystyle Y = 1}$X+1=Y-1+-

Reais e símbolos de função podem ser combinados, levando a termos que são expressões sobre reais e símbolos de função aplicados a outros termos. Formalmente, variáveis ​​e constantes reais são expressões, como qualquer operador aritmético sobre outras expressões. Variáveis, constantes (símbolos de função zero-aridade) e expressões são termos, como qualquer símbolo de função aplicado a termos. Em outras palavras, os termos são construídos sobre expressões, enquanto as expressões são construídas sobre números e variáveis. Nesse caso, as variáveis ​​variam em termos e números reais . Em outras palavras, uma variável pode assumir um número real como valor, enquanto outra pode receber um termo.

A igualdade de dois termos pode ser simplificada usando as regras para termos de árvore se nenhum dos dois termos for uma expressão real. Por exemplo, se os dois termos têm o mesmo símbolo de função e número de subtermos, sua restrição de igualdade pode ser substituída pela igualdade de subtermos.

Domínios finitos

A terceira classe de restrições usada na programação de lógica de restrição é a dos domínios finitos. Os valores das variáveis ​​são, neste caso, retirados de um domínio finito, geralmente de números inteiros . Para cada variável, um domínio diferente pode ser especificado: X::[1..5]por exemplo, significa que o valor de Xestá entre 1e 5. O domínio de uma variável também pode ser dado enumerando todos os valores que uma variável pode assumir; portanto, a declaração de domínio acima também pode ser escrita X::[1,2,3,4,5]. Essa segunda maneira de especificar um domínio permite domínios que não são compostos de inteiros, como X::[george,mary,john]. Se o domínio de uma variável não for especificado, será considerado o conjunto de inteiros representáveis ​​na linguagem. Um grupo de variáveis ​​pode receber o mesmo domínio usando uma declaração como [X,Y,Z]::[1..5].

O domínio de uma variável pode ser reduzido durante a execução. Na verdade, à medida que o interpretador adiciona restrições ao armazenamento de restrições, ele executa a propagação de restrições para impor uma forma de consistência local , e essas operações podem reduzir o domínio das variáveis. Se o domínio de uma variável ficar vazio, o armazenamento de restrição é inconsistente e o algoritmo retrocede. Se o domínio de uma variável se tornar um singleton , a variável pode receber um valor único em seu domínio. As formas de consistência normalmente aplicadas são consistência de arco , consistência de hiper-arco e consistência de limite . O domínio atual de uma variável pode ser inspecionado usando literais específicos; por exemplo, dom(X,D)descobre o domínio atual Dde uma variável X.

Quanto aos domínios de reais, os functores podem ser usados ​​com domínios de inteiros. Nesse caso, um termo pode ser uma expressão sobre números inteiros, uma constante ou a aplicação de um functor sobre outros termos. Uma variável pode receber um termo arbitrário como um valor, se seu domínio não tiver sido especificado como um conjunto de inteiros ou constantes.

O armazenamento de restrições

O armazenamento de restrições contém as restrições que são atualmente consideradas satisfatórias. Pode-se considerar qual é a substituição atual da programação lógica regular. Quando apenas os termos da árvore são permitidos, o armazenamento de restrições contém restrições no formulário t1=t2; essas restrições são simplificadas pela unificação, resultando em restrições do formulário variable=term; tais restrições são equivalentes a uma substituição.

No entanto, o armazenamento de restrições também pode conter restrições no formulário t1!=t2, se a diferença !=entre os termos for permitida. Quando restrições sobre domínios reais ou finitos são permitidas, o armazenamento de restrições também pode conter restrições específicas de domínio X+2=Y/2, como etc.

O armazenamento de restrições estende o conceito de substituição atual de duas maneiras. Em primeiro lugar, ele não contém apenas as restrições derivadas da comparação de um literal com o cabeçalho de uma nova variante de uma cláusula, mas também as restrições do corpo das cláusulas. Em segundo lugar, ele não contém apenas restrições do formulário, variable=valuemas também restrições na linguagem de restrição considerada. Embora o resultado de uma avaliação bem-sucedida de um programa lógico regular seja a substituição final, o resultado de um programa lógico de restrição é o armazenamento de restrição final, que pode conter restrição da forma variável = valor, mas em geral pode conter restrições arbitrárias.

Restrições específicas de domínio podem chegar ao armazenamento de restrição tanto do corpo de uma cláusula quanto da equação de um literal com um cabeçalho de cláusula: por exemplo, se o intérprete reescrever o literal A(X+2)com uma cláusula cujo cabeçalho variante é A(Y/2), a restrição X+2=Y/2é adicionada a o armazenamento de restrição. Se uma variável aparece em uma expressão de domínio real ou finito, ela só pode assumir um valor em reais ou no domínio finito. Essa variável não pode assumir um termo feito de um functor aplicado a outros termos como um valor. O armazenamento de restrição é insatisfatório se uma variável for obrigada a assumir um valor do domínio específico e um functor aplicado aos termos.

Depois que uma restrição é adicionada ao armazenamento de restrição, algumas operações são realizadas no armazenamento de restrição. As operações realizadas dependem do domínio considerado e das restrições. Por exemplo, a unificação é usada para igualdades de árvore finitas, eliminação de variável para equações polinomiais sobre reais, propagação de restrição para impor uma forma de consistência local para domínios finitos. Essas operações visam tornar o armazenamento de restrições mais simples de ser verificado quanto à satisfatibilidade e resolvido.

Como resultado dessas operações, a adição de novas restrições pode alterar as antigas. É essencial que o intérprete seja capaz de desfazer essas alterações ao retroceder. O método de caso mais simples é o interpretador salvar o estado completo da loja toda vez que fizer uma escolha (ele escolhe uma cláusula para reescrever um objetivo). Existem métodos mais eficientes para permitir que o armazenamento de restrição retorne a um estado anterior. Em particular, pode-se apenas salvar as alterações no armazenamento de restrições feitas entre dois pontos de escolha, incluindo as alterações feitas nas restrições antigas. Isso pode ser feito simplesmente salvando o valor antigo das restrições que foram modificadas; este método é denominado trailing . Um método mais avançado é salvar as alterações feitas nas restrições modificadas. Por exemplo, uma restrição linear é alterada modificando seu coeficiente: salvar a diferença entre o coeficiente antigo e o novo permite reverter uma alteração. Esse segundo método é chamado de retrocesso semântico , porque a semântica da mudança é salva, e não apenas a versão antiga das restrições.

Marcação

Os literais de rotulagem são usados ​​em variáveis ​​sobre domínios finitos para verificar a satisfatibilidade ou a satisfatibilidade parcial do armazenamento de restrições e para encontrar uma atribuição satisfatória. Um literal de rotulagem tem a forma labeling([variables]), em que o argumento é uma lista de variáveis ​​sobre domínios finitos. Sempre que o interpretador avalia tal literal, ele realiza uma pesquisa nos domínios das variáveis ​​da lista para encontrar uma atribuição que satisfaça todas as restrições relevantes. Normalmente, isso é feito por uma forma de retrocesso : as variáveis ​​são avaliadas em ordem, tentando todos os valores possíveis para cada uma delas e retrocedendo quando é detectada inconsistência.

O primeiro uso do literal de rotulagem é para verificar a satisfatibilidade ou satisfatibilidade parcial do armazenamento de restrição. Quando o interpretador adiciona uma restrição ao armazenamento de restrições, ele apenas impõe uma forma de consistência local. Esta operação pode não detectar inconsistência, mesmo se o armazenamento de restrição for insatisfatório. Um literal de rotulagem sobre um conjunto de variáveis ​​impõe uma verificação de satisfatibilidade das restrições sobre essas variáveis. Como resultado, o uso de todas as variáveis ​​mencionadas na loja de restrição resulta na verificação da satisfabilidade da loja.

O segundo uso do literal de rotulagem é realmente determinar uma avaliação das variáveis ​​que satisfaça o armazenamento de restrição. Sem o literal de rotulagem, as variáveis ​​recebem valores apenas quando o armazenamento de restrição contém uma restrição do formulário X=valuee quando a consistência local reduz o domínio de uma variável a um único valor. Um literal de rotulagem sobre algumas variáveis ​​força essas variáveis ​​a serem avaliadas. Em outras palavras, após o literal de rotulação ter sido considerado, todas as variáveis ​​recebem um valor.

Normalmente, os programas de lógica de restrição são escritos de forma que literais de rotulagem sejam avaliados somente depois que tantas restrições quanto possível tenham sido acumuladas no armazenamento de restrições. Isso ocorre porque a rotulagem de literais impõe a pesquisa, e a pesquisa é mais eficiente se houver mais restrições a serem satisfeitas. Um problema de satisfação de restrição é normalmente resolvido por um programa de lógica de restrição com a seguinte estrutura:

solve(X):-constraints(X), labeling(X)
constraints(X):- (all constraints of the CSP)

Quando o interpretador avalia a meta solve(args), ele coloca o corpo de uma nova variante da primeira cláusula na meta atual. Como o primeiro objetivo é constraints(X'), a segunda cláusula é avaliada e esta operação move todas as restrições no objetivo atual e, eventualmente, no armazenamento de restrições. O literal labeling(X')é então avaliado, forçando a busca por uma solução para o armazenamento de restrições. Uma vez que o armazenamento de restrições contém exatamente as restrições do problema original de satisfação de restrições, essa operação busca uma solução para o problema original.

Reformulações de programa

Um determinado programa de lógica de restrição pode ser reformulado para melhorar sua eficiência. A primeira regra é que os literais rotulados devem ser colocados depois que tantas restrições nos literais rotulados forem acumuladas no armazenamento de restrições. Embora em teoria seja equivalente a , a pesquisa realizada quando o interpretador encontra o literal de rotulagem está em um armazenamento de restrição que não contém a restrição . Como resultado, ele pode gerar soluções, tais como , que posteriormente serão descobertas como não satisfazendo essa restrição. Por outro lado, na segunda formulação, a pesquisa é realizada apenas quando a restrição já está no armazenamento de restrições. Como resultado, a pesquisa retorna apenas soluções que são consistentes com ela, aproveitando o fato de que restrições adicionais reduzem o espaço de pesquisa. A(X):-labeling(X),X>0A(X):-X>0,labeling(X)X>0X=-1

Uma segunda reformulação que pode aumentar a eficiência é colocar restrições antes dos literais no corpo das cláusulas. Novamente, e são em princípio equivalentes. No entanto, o primeiro pode exigir mais computação. Por exemplo, se o armazenamento de restrição contém a restrição , o interpretador avalia recursivamente no primeiro caso; se for bem-sucedido, ele descobrirá que o armazenamento de restrição é inconsistente durante a adição . No segundo caso, ao avaliar essa cláusula, o interpretador primeiro adiciona ao armazenamento de restrição e, em seguida, possivelmente avalia . Como o armazenamento de restrições após a adição de acaba sendo inconsistente, a avaliação recursiva de não é realizada de forma alguma. A(X):-B(X),X>0A(X):-X>0,B(X)X<-2B(X)X>0X>0B(X)X>0B(X)

Uma terceira reformulação que pode aumentar a eficiência é a adição de restrições redundantes. Se o programador sabe (por qualquer meio) que a solução de um problema satisfaz uma restrição específica, ele pode incluir essa restrição para causar inconsistência no armazenamento de restrição o mais rápido possível. Por exemplo, se for conhecido de antemão que a avaliação de B(X)resultará em um valor positivo para X, o programador pode adicionar X>0antes de qualquer ocorrência de B(X). Por exemplo, A(X,Y):-B(X),C(X)vai falhar na meta A(-2,Z), mas isso só é descoberto durante a avaliação da submeta B(X). Por outro lado, se a cláusula acima for substituída por , o interpretador retrocede assim que a restrição é adicionada ao armazenamento de restrição, o que acontece antes do início da avaliação de pares. A(X,Y):-X>0,A(X),B(X)X>0B(X)

Regras de tratamento de restrições

As regras de tratamento de restrições foram inicialmente definidas como um formalismo autônomo para especificar solucionadores de restrições e, posteriormente, foram incorporadas à programação lógica. Existem dois tipos de regras de tratamento de restrições. As regras do primeiro tipo especificam que, sob uma determinada condição, um conjunto de restrições é equivalente a outro. As regras do segundo tipo especificam que, sob uma determinada condição, um conjunto de restrições implica em outra. Em uma linguagem de programação de lógica de restrição que suporta regras de manipulação de restrição, um programador pode usar essas regras para especificar possíveis reescritas do armazenamento de restrição e possíveis adições de restrições a ele. A seguir estão exemplos de regras:

A(X) <=> B(X) | C(X)
A(X) ==> B(X) | C(X)

A primeira regra diz que, se B(X)for gerada pela loja, a restrição A(X)pode ser reescrita como C(X). Por exemplo, N*X>0pode ser reescrito como X>0se a loja implicasse nisso N>0. O símbolo se <=>assemelha à equivalência em lógica e informa que a primeira restrição é equivalente à última. Na prática, isso implica que a primeira restrição pode ser substituída pela última.

A segunda regra, em vez disso, especifica que a última restrição é uma consequência da primeira, se a restrição no meio for acarretada pelo armazenamento de restrições. Como resultado, se A(X)estiver no armazenamento de restrição e B(X)for vinculado ao armazenamento de restrição, então C(X)pode ser adicionado ao armazenamento. Diferentemente do caso de equivalência, esta é uma adição e não uma substituição: a nova restrição é adicionada, mas a antiga permanece.

A equivalência permite simplificar o armazenamento de restrições, substituindo algumas restrições por outras mais simples; em particular, se a terceira restrição em uma regra de equivalência for true, e a segunda restrição for implicada, a primeira restrição é removida do armazenamento de restrição. A inferência permite a adição de novas restrições, o que pode levar à prova de inconsistência do armazenamento de restrições e pode geralmente reduzir a quantidade de pesquisa necessária para estabelecer sua satisfatibilidade.

As cláusulas de programação lógica em conjunto com as regras de tratamento de restrições podem ser usadas para especificar um método para estabelecer a satisfatibilidade do armazenamento de restrições. Cláusulas diferentes são usadas para implementar as diferentes escolhas do método; as regras de tratamento de restrição são usadas para reescrever o armazenamento de restrição durante a execução. Como exemplo, pode-se implementar retrocesso com propagação de unidade desta forma. Let holds(L)representa uma cláusula proposicional, na qual os literais na lista Lestão na mesma ordem em que são avaliados. O algoritmo pode ser implementado usando cláusulas para a escolha de atribuir um literal para verdadeiro ou falso e regras de tratamento de restrição para especificar a propagação. Essas regras especificam que holds([l|L])pode ser removido se l=truesegue da loja e pode ser reescrito como holds(L)se l=falsesegue da loja. Da mesma forma, holds([l])pode ser substituído por l=true. Neste exemplo, a escolha do valor para uma variável é implementada usando cláusulas de programação lógica; entretanto, ele pode ser codificado em regras de tratamento de restrições usando uma extensão chamada regras de tratamento de restrições disjuntivas ou CHR ^∨ .

Avaliação ascendente

A estratégia padrão de avaliação de programas lógicos é de cima para baixo e primeiro em profundidade : a partir do objetivo, uma série de cláusulas são identificadas como sendo possivelmente capazes de provar o objetivo e é realizada a recursão sobre os literais de seus corpos. Uma estratégia alternativa é partir dos fatos e usar cláusulas para derivar novos fatos; essa estratégia é chamada de baixo para cima . É considerado melhor do que o de cima para baixo quando o objetivo é produzir todas as consequências de um determinado programa, ao invés de provar um único objetivo. Em particular, encontrar todas as consequências de um programa da maneira padrão de cima para baixo e em profundidade pode não terminar enquanto a estratégia de avaliação de baixo para cima termina.

A estratégia de avaliação ascendente mantém o conjunto de fatos provados até agora durante a avaliação. Este conjunto está inicialmente vazio. Com cada etapa, novos fatos são derivados pela aplicação de uma cláusula do programa aos fatos existentes e são adicionados ao conjunto. Por exemplo, a avaliação ascendente do programa a seguir requer duas etapas:

A(q).
B(X):-A(X).

O conjunto de consequências está inicialmente vazio. Na primeira etapa, A(q)é a única cláusula cujo corpo pode ser provado (porque está vazia) e, A(q)portanto , é adicionada ao conjunto atual de consequências. Na segunda etapa, desde que A(q)comprovada, a segunda cláusula pode ser utilizada e B(q)é adicionada às consequências. Uma vez que nenhuma outra consequência pode ser provada {A(q),B(q)}, a execução termina.

A vantagem da avaliação de baixo para cima sobre a de cima para baixo é que os ciclos de derivações não produzem um loop infinito . Isso ocorre porque adicionar uma consequência ao conjunto atual de consequências que já a contém não tem efeito. Como exemplo, adicionar uma terceira cláusula ao programa acima gera um ciclo de derivações na avaliação de cima para baixo:

A(q).
B(X):-A(X).
A(X):-B(X).

Por exemplo, ao avaliar todas as respostas para a meta A(X), a estratégia de cima para baixo produziria as seguintes derivações:

A(q)
A(q):-B(q), B(q):-A(q), A(q)
A(q):-B(q), B(q):-A(q), A(q):-B(q), B(q):-A(q), A(q)

Em outras palavras, a única consequência A(q)é produzida primeiro, mas então o algoritmo percorre as derivações que não produzem nenhuma outra resposta. De maneira mais geral, a estratégia de avaliação top-down pode percorrer as derivações possíveis, possivelmente quando existem outras.

A estratégia de baixo para cima não tem a mesma desvantagem, pois as consequências que já foram derivadas não têm efeito. No programa acima, a estratégia de baixo para cima começa a se somar A(q)ao conjunto de consequências; na segunda etapa, B(X):-A(X)é usado para derivar B(q); na terceira etapa, os únicos fatos que podem ser derivados das consequências atuais são A(q)e B(q), que, entretanto, já estão no conjunto de consequências. Como resultado, o algoritmo para.

No exemplo acima, os únicos fatos usados ​​foram literais básicos. Em geral, toda cláusula que contém apenas restrições no corpo é considerada um fato. Por exemplo, uma cláusula também A(X):-X>0,X<10é considerada um fato. Para esta definição estendida de fatos, alguns fatos podem ser equivalentes, embora não sintaticamente iguais. Por exemplo, A(q)é equivalente a A(X):-X=qe ambos são equivalentes a A(X):-X=Y, Y=q. Para resolver esse problema, os fatos são traduzidos para uma forma normal em que o cabeçalho contém uma tupla de variáveis ​​totalmente diferentes; dois fatos são então equivalentes se seus corpos são equivalentes nas variáveis ​​da cabeça, ou seja, seus conjuntos de soluções são os mesmos quando restritos a essas variáveis.

Conforme descrito, a abordagem de baixo para cima tem a vantagem de não considerar as consequências que já foram derivadas. No entanto, ele ainda pode derivar consequências que são acarretadas por aqueles já derivados, embora não sejam iguais a nenhum deles. Por exemplo, a avaliação ascendente do programa a seguir é infinita:

A(0).
A(X):-X>0.
A(X):-X=Y+1, A(Y).

O algoritmo de avaliação ascendente primeiro deriva que A(X)é verdadeiro para X=0e X>0. Na segunda etapa, o primeiro fato com a terceira cláusula permite a derivação de A(1). Na terceira etapa, A(2)é derivado, etc. No entanto, esses fatos já estão implicados pelo fato de que A(X)é verdadeiro para qualquer não negativo X. Essa desvantagem pode ser superada verificando os fatos de implicação que devem ser adicionados ao conjunto atual de consequências. Se a nova consequência já estiver associada ao conjunto, ela não será adicionada a ele. Uma vez que os fatos são armazenados como cláusulas, possivelmente com "variáveis ​​locais", a vinculação é restrita às variáveis ​​de suas cabeças.

Programação de lógica de restrição simultânea

As versões simultâneas da programação de lógica de restrição têm como objetivo programar processos simultâneos em vez de resolver problemas de satisfação de restrição . Metas na programação de lógica de restrição são avaliadas simultaneamente; um processo concorrente é, portanto, programado como a avaliação de uma meta pelo intérprete .

Sintaticamente, os programas lógicos de restrições concorrentes são semelhantes aos programas não concorrentes, sendo a única exceção que as cláusulas incluem guardas , que são restrições que podem bloquear a aplicabilidade da cláusula sob algumas condições. Semanticamente, a programação de lógica de restrição simultânea difere de suas versões não simultâneas porque uma avaliação de objetivo se destina a realizar um processo simultâneo em vez de encontrar uma solução para um problema. Mais notavelmente, essa diferença afeta como o interpretador se comporta quando mais de uma cláusula é aplicável: a programação de lógica de restrição não concorrente tenta recursivamente todas as cláusulas; a programação de lógica de restrição simultânea escolhe apenas um. Este é o efeito mais evidente de uma direcionalidade pretendida do intérprete, que nunca revisa uma escolha feita anteriormente. Outros efeitos disso são a possibilidade semântica de ter um objetivo que não pode ser provado enquanto toda a avaliação não falhar, e uma forma particular de equacionar um objetivo e um cabeçalho de cláusula.

Formulários

A programação de lógica de restrição foi aplicada a vários campos, como programação automatizada , inferência de tipo , engenharia civil , engenharia mecânica , verificação de circuito digital , controle de tráfego aéreo , finanças e outros.

História

A programação lógica de restrição foi introduzida por Jaffar e Lassez em 1987. Eles generalizaram a observação de que os termos equações e desequilíbrios do Prolog II eram uma forma específica de restrição e generalizaram essa ideia para linguagens de restrição arbitrárias. As primeiras implementações desse conceito foram Prolog III , CLP (R) e CHIP .

Veja também

• BProlog
• BNR Prolog (também conhecido como CLP (BNR))
• tchau
• CLP (R)
• Oz Mozart distribuído
• Eclipse
• GNU Prolog
• SWI-Prolog

Referências

• Dechter, Rina (2003). Processamento de restrições . Morgan Kaufmann. ISBN 1-55860-890-7. ISBN  1-55860-890-7
• Apt, Krzysztof (2003). Princípios de programação de restrições . Cambridge University Press. ISBN 0-521-82583-0. ISBN  0-521-82583-0
• Marriott, Kim; Peter J. Stuckey (1998). Programação com restrições: uma introdução . MIT Press. ISBN  0-262-13341-5
• Frühwirth, Thom; Slim Abdennadher (2003). Princípios básicos da programação de restrições . Springer. ISBN 3-540-67623-6. ISBN  3-540-67623-6
• Jaffar, Joxan; Michael J. Maher (1994). "Programação lógica de restrições: um levantamento" . Journal of Logic Programming . 19/20: 503–581. doi : 10.1016 / 0743-1066 (94) 90033-7 .
• Colmerauer, Alain (1987). "Abrindo o Universo Prolog III". Byte . Agosto.

Referências