Programação lógica de restrição

Da Wikipédia, a enciclopédia livre
Ir para a navegação Saltar para pesquisar

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 na programação lógica 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 lógica regular, os programas são consultados 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íveis e literais que podem ser provados usando outras cláusulas. A execução é realizada por um intérprete, que parte do objetivo e varre recursivamente as cláusulas tentando provar o objetivo. As restrições encontradas durante essa varredura são colocadas em um conjunto chamado armazenamento de restrições . Se esse conjunto for insatisfatível, o intérprete retrocede , tentando usar outras cláusulas para provar o objetivo. Na prática, a satisfatibilidade do armazenamento de restrições pode ser verificada usando um algoritmo incompleto, que nem sempre detecta inconsistências.

Visão geral

Formalmente, os programas lógicos de restrição são como programas lógicos regulares, mas o corpo de cláusulas pode conter restrições, além dos literais de programação lógica regular. Como 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 lógica regular, avaliar um objetivo como A(X,1)requer avaliar o corpo da última cláusula com Y=1. Como na programação lógica regular, isso, por sua vez, requer provar o 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 aterrado e execução do programa irá falhar se não for esse 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 depois verificar se o valor resultante de Xé positivo, o intérprete armazena a restrição X>0e, em seguida, procede 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 B(X,1)a conclusão da avaliação de.

Em geral, a avaliação de um programa de lógica de restrição procede como um programa de lógica regular. No entanto, as restrições encontradas durante a avaliação são colocadas em um conjunto chamado armazenamento de restrições. Como exemplo, a avaliação do objetivo A(X,1)procede avaliando o corpo da primeira cláusula com Y=1; essa avaliação aumenta X>0o armazenamento de restrições e exige que a meta B(X,1)seja comprovada. Ao tentar provar esse objetivo, a primeira cláusula é aplicada, mas sua avaliação adiciona X<0ao armazenamento de restrições. 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ção. A avaliação da segunda cláusula acrescenta X=1eY>0para o armazenamento de restrições. Como o armazenamento de restrições é satisfatível e nenhum outro literal resta para provar, o interpretador para com a solução X=1, Y=1.

Semântica

A semântica de programas de lógica de restrição pode ser definida em termos de um interpretador virtual que mantém um pardurante 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 interpretador está tentando provar e também pode conter algumas restrições que ele está tentando satisfazer; o armazenamento de restrições contém todas as restrições que o interpretador assumiu como satisfatíveis até agora.

Inicialmente, o objetivo atual é o objetivo e o armazenamento de restrições está vazio. O intérprete procede removendo o primeiro elemento do objetivo atual e analisando-o. Os detalhes desta análise são explicados abaixo, mas no final esta análise pode produzir uma rescisão bem-sucedida 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ções. O intérprete retrocede se uma falha for gerada. Uma terminação bem-sucedida é gerada quando a meta atual está vazia e o armazenamento de restrições é satisfatível.

Os detalhes da análise de um literal removido do objetivo são os seguintes. Depois de remover este literal da frente do objetivo, verifica-se se é uma restrição ou um literal. Se for uma restrição, ela será adicionada ao armazenamento de restrições. Se for um literal, escolhe-se uma cláusula cujo núcleo tenha o mesmo predicado do literal; a cláusula é reescrita substituindo suas variáveis ​​por novas variáveis ​​(variáveis ​​que não ocorrem no objetivo): 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 cabeça da variante fresca também é colocada na frente do objetivo.

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

O interpretador provou o objetivo quando o objetivo atual está vazio e o armazenamento de restrição não é detectado como insatisfatível. O resultado da execução é o conjunto atual de restrições (simplificadas). Este conjunto pode incluir restrições comoque forçam as variáveis ​​a um valor específico, mas também podem incluir restrições comoque apenas ligava variáveis ​​sem dar a elas um valor específico.

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/armazenamento, anotado. Tal par afirma a possibilidade de passar do estadodeclarar. Tal transição é possível em três casos possíveis:

  • um elemento de G é uma restrição C ,e; em outras palavras, uma restrição pode ser movida do objetivo para o repositório de restrições
  • um elemento de G é um literal, existe uma cláusula que, reescrita usando novas variáveis, é,é G comsubstituí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 no núcleo, adicionando o corpo da nova variante e as igualdades de termos acima ao objetivo
  • S esão equivalentes de acordo com a semântica de restrição específica

Uma sequência de transições é uma derivação. Um objetivo G pode ser provado se existe uma derivação deparapara algum armazenamento de restrição satisfatível S . Essa semântica formaliza as possíveis evoluções de um interpretador que escolhe arbitrariamente o literal do objetivo a ser processado e a cláusula para substituir os literais. Em outras palavras, um objetivo é provado sob essa semântica se existe uma sequência de escolhas de literais e cláusulas, dentre as muitas possíveis, que levam a um objetivo vazio e a um armazenamento satisfatível.

Os intérpretes reais processam os elementos de objetivo 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 são escritas e reescrevem o armazenamento de restrição quando ele é modificado.

O terceiro tipo de transição possível é a substituição do armazenamento de restrições por um equivalente. Essa substituição é limitada àquelas feitas por métodos específicos, como propagação de restrições . 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 de 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ções for insatisfatível, essa simplificação pode detectar essa insatisfatibilidade algumas vezes, mas nem sempre.

O resultado da avaliação de uma meta em relação a um programa de lógica de restrição é definido se a meta for comprovada. Neste caso, existe uma derivação do par inicial para um par onde o objetivo é vazio. 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 assumidas como satisfatíveis para provar o objetivo. Em outras palavras, o objetivo é comprovado para todas as avaliações de variáveis ​​que satisfazem essas restrições.

A igualdade par a par de termos de dois literais é frequentemente denotada de forma compacta por: esta é uma abreviação para as restrições. Uma variante comum da semântica para programação lógica de restrição adicionadiretamente para o armazenamento de restrições em vez de para a meta.

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 que está sempre presente é a igualdade de termos. Tais restrições são necessárias porque o interpretador adiciona t1=t2ao objetivo sempre que um literal P(...t1...)é substituído pelo corpo de uma nova variante de cláusula cujo núcleo é P(...t2...).

Termos de á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. Termos são variáveis, constantes e símbolos de função aplicados a outros termos. As únicas restrições consideradas são igualdades e desiguais entre os termos. A igualdade é particularmente importante, pois restrições como t1=t2essas são frequentemente geradas pelo intérprete. Restrições de igualdade em termos podem ser simplificadas, o que é resolvido, via 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 os mesmos 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 funtor, 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 no armazenamento de meta e restrição atual, 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.

Nesta forma de satisfação de restrições, 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. Neste caso, cada variável só pode tomar um número real como valor.

Para ser preciso, termos são expressões sobre variáveis ​​e constantes reais. A igualdade entre termos é um tipo de restrição que está sempre presente, pois o intérprete gera igualdade de termos durante a execução. Como exemplo, se o primeiro literal do objetivo atual for A(X+1)e o interpretador tiver escolhido uma cláusula que está A(Y-1):-Y=1após a reescrita são 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: X+1=Y-1não é insatisfatível apenas porque a primeira expressão é construída usando +e a segunda usando -.

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 de 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 sobre números e termos reais . Em outras palavras, uma variável pode receber um número real como valor, enquanto outra recebe 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 tiverem 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 usadas na programação lógica de restrições é a de domínios finitos. Os valores das variáveis ​​são, neste caso, retirados de um domínio finito, geralmente o 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 pela enumeração de 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, comoX::[george,mary,john]. Se o domínio de uma variável não for especificado, supõe-se que seja 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. De fato, à 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ções é inconsistente e o algoritmo retrocede. Se o domínio de uma variável se tornar um singleton , a variável pode receber o valor exclusivo em seu domínio. As formas de consistência normalmente impostas são consistência de arco , consistência de hiper-arco e consistência vinculada . 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, functores podem ser usados ​​com domínios de inteiros. Nesse caso, um termo pode ser uma expressão sobre inteiros, uma constante ou a aplicação de um functor sobre outros termos. Uma variável pode tomar um termo arbitrário como valor, se seu domínio não tiver sido especificado para ser um conjunto de inteiros ou constantes.

O armazenamento de restrições

O repositório de restrições contém as restrições que atualmente são consideradas satisfatíveis. Pode-se considerar qual é a substituição atual para programação lógica regular. Quando apenas termos de árvore são permitidos, o armazenamento de restrições contém restrições no formato t1=t2; essas restrições são simplificadas pela unificação, resultando em restrições da forma 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 reais ou domínios finitos são permitidas, o armazenamento de restrições também pode conter restrições específicas de domínio, como X+2=Y/2, etc.

O armazenamento de restrições estende o conceito de substituição de corrente de duas maneiras. Primeiro, ele não contém apenas as restrições derivadas da igualdade de um literal com a cabeça de uma nova variante de uma cláusula, mas também as restrições do corpo das cláusulas. Em segundo lugar, não contém apenas restrições da forma, variable=valuemas também restrições sobre a linguagem de restrição considerada. Enquanto o resultado de uma avaliação bem-sucedida de um programa de lógica regular é a substituição final, o resultado de um programa de lógica de restrição é o armazenamento de restrição final, que pode conter restrição do formato 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ções tanto do corpo de uma cláusula quanto da igualdade de um literal com um cabeçalho de cláusula: por exemplo, se o interpretador reescrever o literal A(X+2)com uma cláusula cujo cabeçalho de variante fresco é A(Y/2), a restrição X+2=Y/2é adicionada a o armazenamento de restrições. Se uma variável aparece em uma expressão de domínio real ou finito, ela só pode assumir um valor no domínio real ou finito. Tal variável não pode tomar como valor um termo feito de um functor aplicado a outros termos. O armazenamento de restrições é insatisfatório se uma variável for obrigada a receber um valor do domínio específico e um functor aplicado aos termos.

Depois que uma restrição é adicionada ao repositório de restrições, algumas operações são executadas no repositório de restrições. Quais operações são executadas depende do domínio e das restrições consideradas. Por exemplo, a unificação é usada para igualdades de árvores finitas, eliminação de variáveis ​​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 quando retroceder. O método de caso mais simples é o intérprete salvar o estado completo do armazenamento 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ções 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; esse método é chamado de trailing. Um método mais avançado é salvar as alterações que foram 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 alteração é salva em vez da versão antiga apenas das restrições.

Rotulagem

Os literais de rotulagem são usados ​​em variáveis ​​sobre domínios finitos para verificar a satisfatibilidade ou satisfatibilidade parcial do armazenamento de restrições e para encontrar uma atribuição satisfatória. Um literal de rotulagem é da forma labeling([variables]), onde o argumento é uma lista de variáveis ​​sobre domínios finitos. Sempre que o interpretador avalia tal literal, ele realiza uma busca 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 a inconsistência é detectada.

O primeiro uso do literal de rotulagem é verificar a satisfatibilidade real ou satisfatibilidade parcial do armazenamento de restrições. Quando o interpretador adiciona uma restrição ao armazenamento de restrições, ele apenas impõe uma forma de consistência local a ela. Essa 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, usar todas as variáveis ​​mencionadas no armazenamento de restrições resulta na verificação da satisfatibilidade do armazenamento.

O segundo uso do literal de rotulagem é realmente determinar uma avaliação das variáveis ​​que satisfaçam o armazenamento de restrições. Sem o literal de rotulagem, as variáveis ​​recebem valores somente quando o armazenamento de restrições 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 rotulagem ter sido considerado, todas as variáveis ​​recebem um valor.

Normalmente, os programas de lógica de restrição são escritos de tal forma que os literais de rotulagem são avaliados somente depois que o maior número possível de restrições for acumulado no armazenamento de restrições. Isso ocorre porque os literais de rotulagem impõem a pesquisa, e a pesquisa é mais eficiente se houver mais restrições a serem satisfeitas. Um problema de satisfação de restrição é tipicamente resolvido por um programa de lógica de restrição com a seguinte estrutura:

resolver ( X ):- restrições ( X ),  rotular ( X ) 
restrições ( X ):-  ( todas  as restrições  do  CSP ) 

Quando o intérprete avalia o objetivo solve(args), ele coloca o corpo de uma nova variante da primeira cláusula no objetivo atual. Como o primeiro objetivo é constraints(X'), a segunda cláusula é avaliada e essa 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 uma busca por uma solução do armazenamento de restrições. Como 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 do problema original.

Reformulações do programa

Um determinado programa de lógica de restrição pode ser reformulado para melhorar sua eficiência. Uma 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 que é executada 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, pode gerar soluções, comoA(X):-labeling(X),X>0A(X):-X>0,labeling(X)X>0X=-1, que mais tarde se descobriu que não satisfaziam essa restrição. Por outro lado, na segunda formulação a busca é realizada apenas quando a restrição já está no repositório de restrições. Como resultado, a pesquisa retorna apenas soluções consistentes com ela, aproveitando o fato de que restrições adicionais reduzem o espaço de pesquisa.

Uma segunda reformulação que pode aumentar a eficiência é colocar restrições antes de 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 contiver a restrição , o interpretador avaliará recursivamente no primeiro caso; se for bem-sucedido, ele descobrirá que o armazenamento de restrição é inconsistente ao adicionar . 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 se torna inconsistente, a avaliação recursiva de não é realizada. 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ções 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 poderá adicionar X>0antes de qualquer ocorrência de B(X). Como exemplo, A(X,Y):-B(X),C(X)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 intérprete retrocede assim que a restriçãoA(X,Y):-X>0,A(X),B(X)X>0é adicionado ao armazenamento de restrições, o que acontece antes do início da avaliação de B(X)even.

Regras de manipulação de restrições

As regras de manipulação 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 manipulação de restrições. As regras do primeiro tipo especificam que, sob uma dada condição, um conjunto de restrições é equivalente a outro. As regras do segundo tipo especificam que, sob uma dada condição, um conjunto de restrições implica em outro. Em uma linguagem de programação de lógica de restrição que suporta regras de manipulação de restrições, um programador pode usar essas regras para especificar possíveis reescritas do armazenamento de restrições e possíveis adições de restrições a ele. Seguem regras de exemplo:

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

A primeira regra diz que, se B(X)for acarretado pelo store, a restrição A(X)pode ser reescrita como C(X). Como exemplo, N*X>0pode ser reescrito como X>0se a loja implicasse que N>0. O símbolo <=>se assemelha à equivalência na 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 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 repositório de restrições e B(X)for vinculado ao repositório de restrições, C(X)poderá ser adicionado ao repositório. Diferentemente do caso de equivalência, trata-se de uma adição e não de 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 será removida do armazenamento de restrições. 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 geralmente pode reduzir a quantidade de busca necessária para estabelecer sua satisfatibilidade.

Cláusulas de programação lógica em conjunto com regras de manipulação 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 manipulação de restrições são usadas para reescrever o armazenamento de restrições durante a execução. Como exemplo, pode-se implementar o retrocesso com propagação de unidades dessa maneira. 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 a verdadeiro ou falso e regras de manipulação de restrições para especificar a propagação. Essas regras especificam que holds([l|L])pode ser removido sel=truesegue do store, e pode ser reescrito como holds(L)se l=falsesegue do store. Da mesma forma, holds([l])pode ser substituído por l=true. Neste exemplo, a escolha do valor de uma variável é implementada usando cláusulas de programação lógica; no entanto, 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 de baixo para cima

A estratégia padrão de avaliação de programas lógicos é top-down e depth-first : a partir do objetivo, são identificadas várias cláusulas como sendo possivelmente capazes de provar o objetivo, e a recursão sobre os literais de seus corpos é realizada. 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 que o top-down 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 primeiro em profundidade pode não terminar enquanto a estratégia de avaliação de baixo para cima termina.

A estratégia de avaliação bottom-up mantém o conjunto de fatos comprovados até o momento durante a avaliação. Este conjunto está inicialmente vazio. A cada etapa, novos fatos são derivados pela aplicação de uma cláusula de programa aos fatos existentes e são adicionados ao conjunto. Por exemplo, a avaliação de baixo para cima do programa a seguir requer duas etapas:

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

O conjunto de consequências é inicialmente vazio. No primeiro passo, A(q)é a única cláusula cujo corpo pode ser provado (porque está vazio), e, A(q)portanto, é adicionado ao conjunto atual de consequências. Na segunda etapa, uma vez que A(q)está provado, a segunda cláusula pode ser usada e B(q)é adicionada às consequências. Como nenhuma outra consequência pode ser provada a partir de {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 top-down:

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 de cima para baixo pode alternar entre possíveis derivações, possivelmente quando existem outras.

A estratégia de baixo para cima não tem a mesma desvantagem, pois as consequências já derivadas não têm efeito. No programa acima, a estratégia de baixo para cima começa a 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, no entanto, já estão no conjunto de consequências. Como resultado, o algoritmo pára.

No exemplo acima, os únicos fatos usados ​​foram literais de base. Em geral, toda cláusula que contém apenas restrições no corpo é considerada um fato. Por exemplo, uma cláusula A(X):-X>0,X<10também é 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 em uma forma normal na qual a cabeça 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 consequências já derivadas. No entanto, ainda pode derivar consequências que são acarretadas por aquelas já derivadas, embora não sejam iguais a nenhuma delas. Como exemplo, a avaliação de baixo para cima do seguinte programa é infinita:

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

O algoritmo de avaliação de baixo para cima 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). No terceiro passo, 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 pela verificação de fatos de vinculação que devem ser adicionados ao conjunto atual de consequências. Se a nova consequência já está implicada no conjunto, ela não é adicionada a ele. Como 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 lógica de restrição concorrente

As versões concorrentes da programação lógica de restrições visam a programação de processos simultâneos em vez de resolver problemas de satisfação de restrições . Os objetivos na programação lógica de restrição são avaliados simultaneamente; um processo concorrente é, portanto, programado como a avaliação de um objetivo pelo intérprete .

Sintaticamente, os programas lógicos de restrições simultâneas são semelhantes aos programas não simultâneos, com a única exceção de 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 lógica de restrição concorrente difere de suas versões não concorrentes porque uma avaliação de objetivo destina-se a realizar um processo concorrente 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 lógica de restrição não concorrente tenta recursivamente todas as cláusulas; a programação lógica de restrição concorrente escolhe apenas um. Este é o efeito mais evidente de uma direcionalidade pretendidado 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 maneira particular de igualar um objetivo e um núcleo de oração.

Aplicativos

A programação de lógica de restrição tem sido aplicada a uma série de campos, como agendamento automatizado , [1] inferência de tipos , [2] engenharia civil , engenharia mecânica , verificação de circuitos digitais , controle de tráfego aéreo , finanças e outros. [ citação necessária ]

História

A programação em lógica de restrição foi introduzida por Jaffar e Lassez em 1987. [3] Eles generalizaram a observação de que o termo equações e desequações do Prolog II eram uma forma específica de restrições e generalizaram essa ideia para linguagens de restrição arbitrárias. As primeiras implementações deste conceito foram Prolog III , CLP(R) e CHIP . [ citação necessária ]

Veja também

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
  • Marriot, Kim; Peter J. Stuckey (1998). Programação com restrições: Uma introdução . Imprensa do MIT. ISBN  0-262-13341-5
  • Frühwirth, Thom; Slim Abdennadher (2003). Fundamentos de programação de restrição . Springer. ISBN 3-540-67623-6. ISBN  3-540-67623-6
  • Jaffar, Joxan; Michael J. Maher (1994). "Programação lógica de restrição: uma pesquisa" . Jornal de Programação Lógica . 19/20: 503-581. doi : 10.1016/0743-1066(94)90033-7 .
  • Colmerauer, Alan (1987). "Abrindo o Universo Prolog III". Byte . Agosto.

Referências

  1. Abdennadher, Slim e Hans Schlenker. " Enfermeira agendamento usando programação lógica de restrição ." AAAI/IAAI. 1999.
  2. Michaylov, Spiro e Frank Pfenning. " Programação Lógica de Ordem Superior como Programação Lógica de Restrição ." PPCP. Vol. 93. 1993.
  3. ^ Jaffar, Joxan e JL. Lassez. " Programação lógica de restrição ." Anais do 14º simpósio ACM SIGACT-SIGPLAN sobre Princípios de linguagens de programação. ACM, 1987.