# Satisfação de restrições

Em inteligência artificial e investigação operacional, satisfação de restrições é um processo de encontrar a solução para um conjunto de restrições que impõe uma série de condições para que variáveis possam ser atendidas. Uma solução é portanto um conjunto de valores que satisfazem as variáveis de forma a atender todas as restrições que existem para o mundo em que se encontram.
As técnicas usadas na resolução de problemas de satisfação de restrições dependem do tipo de restrição inicial que é considerada. Geralmente ocorre o uso de restrições sobre um domínio finito de forma que o problema de satisfação de restrições e identificável como um problema baseado em restrições deste conjunto finito de restrições. Tais problemas são normalmente resolvidos pela execução de um algoritmo de busca, em particular por algoritmos de backtracking ou busca local. Métodos de consistência local também são empregados para tais problemas, e de forma geral tais algoritmos são incompletos. Ou seja eles podem resolver o problema de provar a insatisfabilidade de um conjunto, mas nem sempre são capazes de executar tal operação. A técnica de consistência local também é usada em conjunto com algoritmos de busca para tornar o problema mais simples de ser resolvido. Outros tipos de restrição a serem considerados são os relacionados sob a forma de números reais e racionais; uma vez que, a resolução de problemas nestes mundos é feita por meio da eliminação de variáveis ou do algoritmo simplex.
Satisfação de restrições se originou como um campo da inteligência artificial em meados de 1970. Durante as décadas de 1980 e 1990, foram desenvolvidas a inclusão de tal teoria em linguagens de programação como Prolog e C++.

## O Problema da Satisfação de Restrições

Como inicialmente foi definido em inteligência artificial, existem restrições necessárias para enumerar os possíveis valores que um conjunto de variáveis podem assumir. Informalmente, um domínio finito é um conjunto de elementos arbitrários. Assim um problema de satisfação em tal domínio contém um conjunto de variáveis cujos valores só podem ser definidos sobre o domínio, e um conjunto de limitações, delineando cada restrição para os valores permitidos para tal conjunto de variáveis.
Em algumas circunstâncias, podem existir requisitos adicionais como: uma solução que possa ser interessante não apenas na solução (em questões como velocidade e eficiência computacional requerida para alcançar a resposta) mas também na forma como tal resolução é obtida; Por exemplo, pode-se querer a solução "mais simples" ("simples" em lógica, não no sentido de ser definido de forma precisamente computacional). Como ocorre frequentemente em jogos de lógica como o Sudoku.
Na prática, restrições são geralmente expressas de forma compacta, em vez de listar todos os valores que a variável pode assumir de forma a atender a restrição imposta. Uma das restrições mais usadas (e óbvia) consiste no processo de estabelecimento de que todos os valores das variáveis afetadas devem ser diferentes.
Problemas que podem ser expressos por meio de problemas de satisfação de restrição são o problema das oito damas, o Sudoku e a resolução de diversos outros jogos de lógica, o problema de satisfatibilidade booleana, o problema do agendamento de tarefas e vários outros problemas relacionados a grafos como o problema da coloração de grafos.
Embora não incluídos no problema de satisfação de restrições, as equações e inequações matemáticas são limitados aos valores que eles dispõem e pode ser considerado como uma forma de restrição. Seu domínio é o do conjunto dos números (sejam inteiros, racionais ou reais), que é infinito. Portanto as relações de restrições também podem ser infinitas; por exemplo, $X=Y+1$ tem um número infinito de pares que satisfazem os seus valores. Assim as equações e inequações aritméticas não são consideradas pela definição do "problema de satisfação de restrição", cujo domínio é limitado. Eles são entretanto usados na programação das restrições.
Pode ser mostrado que as equações e inequações presentes em alguns tipos de puzzles lógicos finitos como o Futoshiki ou Kakuro (também conhecido como Cross Sums) podem ser instanciadas como uma restrição não aritmética (veja Pattern-Based Constraint Satisfaction and Logic Puzzles).

### Resolvendo

O problema da satisfação de restrição em domínios infinitos é normalmente resolvido usando um algoritmo de busca. As técnicas mais usadas são variantes do backtracking, consistência local, e busca local. Tais técnicas são usadas em problemas de restrição que não são lineares.
Eliminação de variáveis e o algoritmo simplex são usados para resolver problemas lineares e polinomiais em equações e inequações, e problemas que tenham variáveis com domínio infinito. Eles são normalmente resolvidos por como problemas de otimização com suas funções de otimização e um número de restrições violadas.

### Complexidade

Resolver o problema de satisfação de restrições em um domínio infinito é um problema NP-completo em relação ao tamanho do domínio. Pesquisas tem mostrado a existência de um número de subproblemas tratáveis assim algumas restrições são permitidas nas restrições das relações, algumas requerem que o escopo seja construído sobre a forma de árvore, possibilitando criar uma versão reformulada do prolema. Pesquisas também tem estabelecido relações do problema de satisfação com problemas advindos de outras áreas como a teoria dos modelos finitos.

## Programação com Restrição

A programação com restrições é usada em uma linguagem de programação para codificar e resolver problemas. Isto geralmente é feito pela inclusão de restrições na linguagem de programação, que é chamada de linguagem hospedeira. A programação com restrições se originiou da formalização de igualdade de termos em Prolog II, levando a incorporação de um conjunto de restrições em linguagens de programação lógica. As linguagens mais comuns são Prolog, C++ e Java, mas outras linguagens também fazem um bom uso do conceito.

### Programação lógica com restrições

Um programa lógico com restrições é um programa lógico que contem restrições no corpo das suas cláusulas. Como exemplo temos a clausula A(X):-X>0,B(X) que contem a restrição X>0 no seu corpo. Restrição também podem estar presentes no objetivo. Ou seja, as restrição no objetivo e as cláusulas usadas para provar o objetivo são acumuladas em um conjunto chamado de armazém de restrições. Este conjunto contém a interpretação das restrições que são assumidas como satisfatíveis a fim de se executar uma avaliação. Como resultado , se este conjunto e detectado como insatisfatível, o interpretador retorna ao passo anterior. Equações são termos usados na lógica de programação, são considerados uma forma particular de restrição que podem ser simplificados usado computação unificada. Assim como resultado, o armazém de restrições pode armazenar uma considerável extensão de conceitos de substições lógicas que é usada na lógica de programação regular. Os tipos mais comuns de restrições que são usados na lógica de programação são sobre números inteiros, racionais, reais e sobre domínios infinitos.
Linguagens de programação com restrições lógicas concorrentes também foram desenvolvidas. Elas são significativamente diferentes do uma linguagem de programação com restrições não concorrente uma vez que, visão processos que rodam paralelamente e que podem não terminar. Também temos que a manipulação de restrição de regras pode ser visto como uma forma de programação com restrições lógicas concorrentes, sendo as vezes usados dentro de uma linguagem de programação com restrições não concorrente. Elas permitem a reescrita de restrições e são capazes de inferir novas restrições com base na valoração das condições.

### Toolkits para satisfação de restrições

Toolkits de satisfação de restrições são bibliotecas de software para linguagens de programação imperativa que são usadas para codificar e resolver um problema de satisfação de restrições.
* Cassowary constraint solver, é um projeto de software livre para satisfação de restrições (disponível para C, Java, Pyton e outras linguagens de programação).
* Comet, e um toolkit e uma linguagem de programação para tais problemas.
* Gecode, é um projeto de software livre escrito em C++ e desenvolvido para possibilitar alta eficiencia e qualidade com todo o poder teorico como fundo.
* JaCoP, é um projeto de software livre para o problema de satisfação de restrições.
* Koalog, Um resolvedor de restrições comercial baseado em Java.
* logilab-constraint, e um projeto de software livre escrito em Pyton puro com os algoritmos de propagação para a resolução de problemas de satisfação de restrições.
* MINION, Um projeto de software livre escrito em C++, com uma pequena linguagem cuja proposta e a especificação de modelos/problemas.
* ZDC, uma ferramenta de programação desenvolvida no Computer-Aided Constraint Satisfaction Project para modelar e resolver problemas de satisfação de restrições.

### Outras linguagens de programação com restrições

Toolkits para problemas de restrições são uma forma para incorporação de restrições em uma linguagem de programação imperativa. Entretanto estes são usados apenas como bibliotecas externas para codificar e resolver problemas. Uma abordagem em que as restrições são integradas com uma linguagem de programação imperativa pode ser visto na linguagem de programação Kaleidoscope.
Restrições também podem ser incluídas em linguagens de programação funcional.