Domínios Finitos
Em muitas problemas de interesse, não é possível aceditar
soluções fraccionárias ou reais, mas apenas soluções
inteiras.
Exemplos destas aplicações incluem:
• Planeamento de testes em circuitos digitais
– Para detecção/distinção de avarias
• Gestão da Produção
– quantidades inteiras
• Sequenciação de Tarefas (Scheduling)
• Geração de Horários
• Caixeiro Viajante
– Simples ou Multiplo
1
Domínios Finitos
De uma forma mais geral, as soluções não necessitam
sequer ser numéricas.
Por exemplo, num problema de coloração de grafos (ou
mapas) pretende-se escolher cores que não constituem um
conjunto numérico (nem sequer ordenado, na interpretação
habitual).
Para estes domínios, não existem resolvedores simbólicos
completos, isto é, não existem procedimentos algébricos
que permitam decidir se um problema é possível ou não,
sendo necessário recorrer, em geral, à pesquisa de um
espaço finito de soluções potenciais.
2
Satisfação Booleana - SAT
Um caso particular de domínios finitos, é o caso do domínio
composto pelos valores booleanos, em que as variáveis
podem tomar o valor 0/1.
No domínio da informática, a importância deste domínio é
óbvia: em última análise todos os problemas são compilados
para especificações codificadas em bits numa linguagem
máquina a executar por um processador.
Mais praticamente, um grande número de problemas pode
ser especificado através de um conjunto de expressões
booleanas.
Essas expressões booleanas podem ser colocadas na forma
clausal (conversão para CNF - forma normal conjuntiva).
3
Satisfação Booleana - SAT
Exemplo_1: n-rainhas
Este problema já foi analisado anteriormente. Associandose a ausência/presença de uma rainha numa das n2 casas de
um tabuleiro com n casas de lado, com uma variável 0/1, o
problema é modelado através de um conjunto de dois tipos
de restrições:
•
Deve haver pelo menos, uma rainha num conjunto de
casas (linhas e colunas)
•
Deve haver no máximo uma rainha num conjunto de
casas (linhas, colunas e diagonais).
Estas restrições podem ser modeladas facilmente na forma
clausal.
4
Satisfação Booleana - SAT
R1: Deve haver pelo menos uma rainha num conjunto Q1 a Qn
de casas
•
1 só cláusula:
Q1  Q2  ...  Qn
R2: Deve haver no máximo uma rainha num conjunto Q1 a Qn
de casas
•
Várias (no total de n*(n-1)/2) claúsulas do tipo:
 Q1   Q2
 Q1   Q3
..
 Q1   Qn
...
 Qn-1   Qn
5
Satisfação Booleana - SAT
Exemplo_2: Coloração de Grafos
Dado um grafo não dirigido, garantir que dois nós
adjacentes (ligados por um arco) têm cores diferentes.
Em primeiro lugar há que modelar a cor de um nó do grafo.
Em geral, k cores requerem ceiling(log2(k)) variáveis
booleanas, ou bits, para serem representadas.
Para simplificar, assumamos a existência de 4 cores. Neste
caso, como ceiling(log2(4)) = 2, são necessárias duas
variáveis booleanas para representar 4 cores distintas.
Assim a cor do nó i é codificada com as variáveis booleanas
Ci,1 e Ci,2.
6
Satisfação Booleana - SAT
Exemplo_2: Coloração de Grafos
Em segundo lugar há que modelar as restrições de que nós
adjacentes têm cores diferentes. Considerando os nós i e j,
esta restrição é modelada como
(Ci,1  Cj,1 )  (Ci,2  Cj,2 )
Mas a  b 
(a  b)   (a  b)  (a  b)  (a   b)
Assim a restrição
[(Ci,1  Cj,1 )  ( Ci,1   Cj,1 )]  [(Ci,2  Cj,2 )  ( Ci,2   Cj,2 )]
É equivalente às 4 cláusulas
Ci,1  Cj,1  Ci,2  Cj,2
 Ci,1   Cj,1  Ci,2  Cj,2
Ci,1  Cj,1   Ci,2   Cj,2
 Ci,1   Cj,1   Ci,2   Cj,2
7
Satisfação Booleana - SAT
Exemplo_3: Saco Mochila (Decisão)
Dado um conjunto de n objectos, cada um com um volume
(inteiro) vi e um valor zi, verificar se numa mochila com
capacidade (em volume) V podem ser colocado um conjunto
de objectos com valor total não inferior a Z.
Este problema pode ser modelado através de n variáveis
booleanas, Xi, em que cada uma modela a selecção (1) ou
não(0) do objecto para ser colocado na mochila.
Assim, a restrição de não exceder o peso pode ser
expressa como
v1 X1 + v2 X2 + ... + vn Xn =< V
8
Satisfação Booleana - SAT
Exemplo_3: Saco Mochila (Decisão)
v1 X1 + v2 X2 + ... + vn Xn =< V
Para modelar esta restrição em cláusulas, há que modelar a
• a multiplicação de um inteiro por um bit (0/1)
• a soma de valores inteiros
• a comparação (=<) de dois inteiros
Apesar de “trabalhosa”, esta modelação para a forma
clausal é facilmente efectuada.
9
Satisfação Booleana - SAT
Exemplo_3: Saco Mochila (Decisão)
• a multiplicação de um inteiro por um bit (0/1)
Dado o inteiro B representado em binário pelos bits Bk a
B0, a multiplicação desse inteiro pelo bit X origina o inteiro
representado pelos bits Mk a M0, tais que Mi = X  Bi.
Esta igualdade pode ser imposta através das cláusulas
(X=0  Mi=0)  ( X=1  Mi=Bi)
 (X=0  X=1)(X=0  Mi=Bi)(Mi=0  X=1)(Mi=0  Mi = Bi)
 (X  Mi= Bi)  ( Mi=Bi)  ( Mi  X)
 (Mi  Bi) ( Mi   Bi)  ( Mi  X)
 (Mi   Bi)  (  Mi  Bi)  ( Mi  X)
10
Satisfação Booleana - SAT
Exemplo_3: Saco Mochila (Decisão)
• a soma de valores inteiros
Dados os inteiros A e B representados em binário pelos
bits ak/bk a ak/b0, a sua soma S pode ser obtida através
das restrições
Primeiro bit
S0 = A0  B0
Último bit
Sn+1 = Cn+1
Outros bits
Si = Ai  Bi  Ci
C1 = A0  B0
Ci+1 = (AiBi)  (AiCi)  (BiCi)
que se colocam na forma clausal de uma forma semelhante.
11
Satisfação Booleana - SAT
Primeiro bit
• S0 = A0  B0
 (S0  (A0  B0))  (S0  (A0  B0))
 (S0((A0B0)(A0 B0)))  ( S0 ((A0B0)(A0B0)))
 (S0A0B0 ) (S0A0B0)  (S0A0B0)  (S0A0B0)
• C1 = A0  B0
 (C1  (A0  B0))  (C1  (A0  B0))
 (C1  A0  B0)  (C1  A0 )  (C1  B)
Último bit
• Sn+1 = Cn+1
 (Sn+1   Cn+1)  ( Sn+1  Cn+1)
12
Satisfação Booleana - SAT
Outros bits
• Si = Ai  Bi  Ci
 (Si  (Ai  Bi  Ci))  (Si  (Ai  Bi  Ci))
...
 (Si  Ai  Bi  Ci)  (Si  Ai  Bi  Ci) 

(Si  Ai  Bi  Ci)  (Si  Ai  Bi  Ci) 

(Si  Ai  Bi  Ci)  (Si  Ai  Bi  Ci) 

(Si  Ai  Bi  Ci)  (Si  Ai  Bi  Ci)
• Ci+1 = (AiBi)  (AiCi)  (BiCi)
...
 (Ai  Bi  Ci+1)  (Ai  Bi  Ci+1) 

(Ai  Ci  Ci+1)  (Ai  Ci  Ci+1) 

(Bi  Ci  Ci+1)  (Bi  Ci  Ci+1)
13
Satisfação Booleana - SAT
Exemplo_3: Saco Mochila (Decisão)
• a comparação (=<) de dois inteiros
Dados os inteiros A e B representados em binário pelos
bits Ak/Bk a A0/B0, a sua comparação (A =< B) pode ser
feita através das variáveis booleanas X0 a Xk, em que Xi
indica que Ai ... A0 =< Bi ... B0. Assim deveremos ter
• X0 = (A0 =< B0)

...

(A0  B0  X0)  (A0  X0)  (B0  X0)
• Xk = (Ak< Bk)  ((Ak=Bk)  Xk-1)
para k 1
(Ai  Xi  Xi-1)  (Ai  Xi  Xi-1) 
(Ai  Bi  Xi )  (Ai  Bi  Xi )
(Bi  Xi  Xi-1)  (Bi  Xi  Xi-1)
14
SAT e 3SAT
Apesar de algumas cláusulas conterem mais de 3 variáveis,
a satisfação de uma cláusula com mais de 3 variáveis pode
ser sempre convertida, com introdução de variáveis extra,
na satisfação de várias cláusulas com apenas 3 variáveis.
Exemplo: A satisfação de uma cláusula
P: A  B  C  D
é equivalente à satisfação das cláusulas Q e R abaixo
Q: A  B  X
e
R: C  D   X
Para provar este resultado temos de provar que:
• P  Q,R: sempre que P puder ser satisfeita Q e R tambem podem
• Q,R  P: sempre que Q e R puderem ser satisfeitas P também pode
15
SAT e 3SAT
P: A  B  C  D

Q: A  B  X
e
R: C  D   X
Se P pode ser satisfeito, então pelo menos uma variável A a
D toma o valor 1. Sem perda de generalidade consideremos
que é A(C). Então a cláusula Q já está satisfeita. A outra
cláusula, R, é satisfeita com X = 0(1).
Q: A  B  X
e
R: C  D   X

P: A  B  C  D
Como X = 0 ou X=1, se Q e R são satisfeitas, então uma das
cláusulas A  B (se X=0) ou C  D (se X=1) é satisfeita.
Mas desta forma uma das variáveis A a D toma o valor 1,
garantindo a satisfação da cláusula P: A  B  C  D.
16
Importância de SAT
Como se pode constatar, vários problemas de decisão
podem ser modelados na forma de problemas SAT.
Na realidade, qualquer problema de decisão pode ser
modelado como um problema de satisfação booleana.
Problema
de Decisão
Problema
SAT
Desta forma, um algoritmo genérico para resolver este tipo
de problemas, resolve qualquer problema de decisão.
A questão que se pode colocar é a de saber se existe um
algoritmo “eficiente” para a resolução do problema de
satisfação booleana (SAT).
17
Importância de SAT
Um problema SAT com n variáveis (mais rigorosamente,
que se pode descrever com uma cadeia de entrada de
comprimento proporcional a n) pode ser resolvido em
tempo polinomial numa máquina não-determinística (isto é,
que adivinha os valores correctos a atribuir às n variáveis
de decisão).
Tais problemas de decisão, de que SAT é um exemplo,
pertencem à classe NP.
Mais concretamente, uma máquina determinística (as que
há!) pode verificar as restrições para uma solução de um
problema de decisão em tempo polinomial, isto é O(nk).
18
Importância de SAT
Considerando-se n variáveis booleanas,
combinações possíveis dos seus valores.
existem
2n
A verificação da satisfazibilidade de um conjunto de
cláusulas com n variáveis pode pois ser feita através de um
procedimento de geração e teste:
•
Gera-se cada uma das 2n combinações de valores;
•
Testa-se cada uma dessas combinações.
Naturalmente este procedimento é muito ineficiente. No
pior caso tem uma complexidade exponencial O(2n).
Naturalmente nem todos os problemas de decisão são tão
complexos.
19
Importância de SAT
Para certos problemas existem algoritmos polinomiais (em
n) que permitem decidir sobre a satisfação do problema.
Alguns problemas, que constituem a classe de problemas P,
são claramente polinomiais.
• Por exemplo, decidir se uma lista corresponde à
ordenação de outra lista com n inteiros pode ser feito
com uma complexidade quadrática O(n2).
Noutros problemas não claramente polinomiais, existem
instâncias particularmente simples.
• Por exemplo, o saco mochila torna-se trivial se todos os
objectos tiverem o mesmo peso (não o mesmo valor!).
Basta escolher primeiro os mais valiosos!
20
Importância de SAT
Naturalmente, todos os problemas P pertencem à classe NP
já que se uma máquina determinística os resolve em tempo
polinomial, por mais forte razão uma máquina não
determinística os consegue resolver nesse tempo.
O que ainda não está demonstrado é que a classe NP
contenha problemas que não são P. Este resultado é, por
ora, uma simples conjectura: P ≠ NP.
Em termos práticos, não foi ainda descoberto um qualquer
algoritmo que resolva qualquer problema SAT em tempo
polinomial (no número de variáveis).
De um ponto de vista teórico, se tal acontecer, o que é
extremamente improvável, então P=NP.
21
Importância de SAT
De um ponto de vista mais prático, se tal improvável
algoritmo fôr descoberto, então todos os problemas de
decisão “interessantes” passarão a ser resolvidos em tempo
polinomial.
Com efeito, basta garantir que para cada problema existe
um algoritmo que o transforme, em tempo polinomial, numa
instância de um problema SAT.
Estas transformações podem normalmente ser feitas de
uma forma semelhante À usada nos exemplos anteriores
(rainhas, coloração de grafos, saco-mochila, etc.).
Este resultado é uma das razões pelas quais o problema
SAT (ou 3SAT) tem sido tão estudado.
22
Importância de SAT
A generalidade da abordagem SAT, na qual qualquer
problemas de decisão pode ser modelado, constitui outra
das razões pelas quais o problema SAT (ou 3SAT) tem sido
tão estudado.
Apesar de ser pouco provável a existência de um algoritmo
que resolva qualquer instância de SAT em tempo polinomial,
existem algoritmos que resolvem muito satisfatoriamente
um grande número de instâncias de problemas SAT.
Em particular, existem resolvedores de SAT que já
conseguem lidar com instâncias de problemas com cerca de
um milhão de variáveis e dez milhões de cláusulas.
23
Resolução de 3SAT
A geração de todas as soluções pode ser obtida pelo
mecanismo de retrocesso de uma linguagem de
programação em lógica.
Exemplo:
rainhas_4(L):geração(L),
teste(L),
report(L).
teste([Q1, Q2, Q3, ..., Q16]):um_ou_menos([Q1,Q2,Q3,Q4]),
um_ou_mais([Q1,Q2,Q3,Q4]),
...
geração([]).
geração([H|T]):membro(H,[1,0]),
geração(T).
um_ou_menos([Q9,Q14]).
24
Resolução de 3SAT
Para simplicidade, no programa rainhas_sat_1gt os testes
foram programados explicitamente.
1ª linha
% um_ou_menos([Q1,Q2,Q3,Q4])
~Q1 # ~Q2,
~Q1 # ~Q3, ~Q2 # ~Q3,
~Q1 # ~Q4, ~Q2 # ~Q4,
~Q3 # ~Q4
% um_ou_mais([Q1,Q2,Q3,Q4]),
Q1 # Q2 # Q3 # Q4,
25
Resolução de 3SAT
Nesse programa rainhas_sat_1gt utilizam-se as facilidades
sintáticas disponíbilizadas pela Pprogramação em Lógica,
nomeadamente a definição de operadores.
% declaração dos operadores booleanos
:- op(300,fy,~).
:- op(400,xfy,#).
% verificação/teste de uma cláusula
X # Y :exp(X # Y, Exp),
Exp >= 1.
exp(X, X):- atomic(X), !.
exp(~X, 1-ExpX):- !,
exp(X, ExpX).
exp(X # Y, ExpX + ExpY):- !,
exp(X, ExpX), exp(Y, ExpY).
26
Resolução de 3SAT - Retrocesso
Muitas potenciais soluções podem ser descartadas apenas
por análise de uma solução parcial. Por exemplo, qualquer
solução com Q1=Q2=1 pode ser descartada, já que não pode
haver 2 rainhas na mesma linha.
Uma forma mais eficiente de verificar a satisfação de um
problema é a utilização de um método construtivo, em que
soluções parciais (em que apenas algumas variáveis têm
valores atribuídos), vão sendo “completadas”, desde que não
violem, por si só, nenhuma restrição.
Se a solução parcial violar restrições, ela não é completada,
explorando-se, por retrocesso (backtracking), alternativas.
27
Resolução de 3SAT - Retrocesso
a
b
c
d
c
c
d
b
b
X
d
a
d
d
c
c
X
d
d
d
d
b
c
c
d
d
d
d
c
d
d
d
Se a combinação a=b=1 não satisfizer uma das restrições,
não são testadas nenhumas combinações que incluam a=b=1.
A “primeira” solução <a,b,c,d>= <1,0,0,1> é encontrada
evitando-se o teste de 6 folhas.
28
Resolução de 3SAT
A completação das soluções parciais pode ser facilmente
obtida pelo mecanismo de retrocesso de uma linguagem de
programação em lógica.
A questão que se coloca aqui é a de garantir que os testes
sejam feitos tão cedo quanto possível. Assim,
•
após instanciar as variáveis Q1 e Q2, da mesma
linha, deverá ser verificado que elas não tomam
ambas o valor 1.
•
...
•
após instanciar a variável Q4 deve ser verificado
que uma de Q1 a Q4 toma o valor 1.
29
Resolução de 3SAT
Para simplificar a exposição, esta verificação é feita de
uma forma explícita no programa rainhas_sat_1bk.
lrainhas_4(_):label(Q1), % 1ª linha
label(Q2),
~Q1 # ~Q2,
label(Q3),
~Q1 # ~Q3, ~Q2 # ~Q3,
label(Q4),
Q1 # Q2 # Q3 # Q4,
~Q1 # ~Q4, ~Q2 # ~Q4, ~Q3 # ~Q4,
...
% onde a atribuição de valor é feita através de
label(Q):- mb(Q,[0,1]).
30
Resolução de 3SAT
Como é fácilmente compreensível, a programação por
retrocesso é muito mais eficiente.
A contabilização quer dos testes feitos quer das
atribuições efectuadas pode ser medida pela inserção de
contadores.
% contagem das atribuições feitas
mb(X,[X|_]):- inc(l).
mb(X,[_|T]):- mb(X,T).
% contagem das testes feitos
X # Y :exp(X # Y, Exp),
inc(t),
Exp >= 1.
31
Propagação de Restrições
Uma alternativa à verificação por backtracking da
compatibilidade entre cada variável e as variáveis passadas
(com valor já atribuído), é geralmente muito vantajoso
eliminar do domínio das variáveis futuras (com valor ainda
por atribuir), os valores incompatíveis com os actualmente
atribuídos.
Esta filosofia permite, em muitos casos:
•
Perceber mais rapidamente a impossibilidade de
completar a solução parcial
•
Retroceder para as causas relevantes da falha
32
Retrocesso
Testes 0
Retrocessos 0
33
Retrocesso
Q1 \= Q2,
L1+Q1 \= L2+Q2,
Testes 0 + 1 = 1
L1+Q2 \= L2+Q1.
Retrocessos 0
34
Retrocesso
Q1 \= Q2,
L1+Q1 \= L2+Q2,
Testes 1 + 1 = 2
L1+Q2 \= L2+Q1.
Retrocessos 0
35
Retrocesso
Q1 \= Q2,
L1+Q1 \= L2+Q2,
Testes 2 + 1 = 3
L1+Q2 \= L2+Q1.
Retrocessos 0
36
Retrocesso
Testes 3 + 1 = 4
Retrocessos 0
37
Retrocesso
Testes 4 + 2 = 6
Retrocessos 0
38
Retrocesso
Testes 6 + 1 = 7
Retrocessos 0
39
Retrocesso
Testes 7 + 2 = 9
Retrocessos 0
40
Retrocesso
Testes 9 + 2 = 11
Retrocessos 0
41
Retrocesso
Testes 11 + 1 + 3 = 15
Retrocessos 0
42
Retrocesso
Testes 15 + 1 + 4 + 2 + 4 = 26
Retrocessos 0
43
Retrocesso
Testes 26 + 1 = 27
Retrocessos 0
44
Retrocesso
Testes 27 + 3 = 30
Retrocessos 0
45
Retrocesso
Testes 30 + 2 = 32
Retrocessos 0
46
Retrocesso
Testes 32 + 4 = 36
Retrocessos 0
47
Retrocesso
Testes 36 + 3 = 39
Retrocessos 0
48
Retrocesso
Testes 39 + 1 = 40
Retrocessos 0
49
Retrocesso
Testes 40 + 2 = 42
Retrocessos 0
50
Retrocesso
Testes 42 + 3 = 45
Retrocessos 0
51
Retrocesso
Falha
6
Retrocede
5
Testes 45
Retrocessos 0
52
Retrocesso
Testes 45
Retrocessos 1
53
Retrocesso
Testes 45 + 1 = 46
Retrocessos 1
54
Retrocesso
Testes 46 + 2 = 48
Retrocessos 1
55
Retrocesso
Testes 48 + 3 = 51
Retrocessos 1
56
Retrocesso
Testes 51 + 4 = 55
Retrocessos 1
57
Retrocesso
Falha
6
Retrocede
5e4
Testes 55+1+3+2+4+3+1+2+3 = 74
Retrocessos 1
58
Retrocesso
Testes 74+2+1+2+3+3= 85
Retrocessos 1+2 = 3
59
Retrocesso
Testes 85 + 1 + 4 = 90
Retrocessos 3
60
Retrocesso
Testes 90 +1+3+2+5 = 101
Retrocessos 3
61
Retrocesso
Testes 101+1+5+2+4+3+6= 122
Retrocessos 3
62
Retrocesso
Falha
8
Retrocede
7
Testes 122+1+5+2+6+3+6+4+1= 150
Retrocessos 3+1=4
63
Retrocesso
Falha
7
Retrocede
6
Testes 150+1+2= 153
Retrocessos 4+1=5
64
Retrocesso
Falha
6
Retrocede
5
Testes 153+3+1+2+3= 162
Retrocessos 5+1=6
65
Retrocesso
Testes 162+2+4= 168
Retrocessos 6+1=7
66
Retrocesso
Falha
6
Retrocede
5
Testes 168+1+3+2+5+3+1+2+3= 188
Retrocessos 7
67
Retrocesso
Falha
5
Retrocede
4
Testes 188+1+2+3+4= 198
Retrocessos 7+1=8
68
Retrocesso
Testes 198 + 3 = 201
Retrocessos 8+1=9
69
Retrocesso
Testes 201+1+4 = 206
Retrocessos 9
70
Retrocesso
Testes 206+1+3+2+5 = 217
Retrocessos 9
71
Retrocesso
Testes 217+1+5+2+5+3+6 = 239
Retrocessos 9
72
Retrocesso
Falha
8
Retrocede
7
Testes 239+1+5+2+4+3+6+7+7= 274
Retrocessos 9+1=1073
Retrocesso
Falha
7
Retrocede
6
Testes 274+1+2= 277
Retrocessos 10+1=11
74
Retrocesso
Falha
6
Retrocede
5
Testes 277+3+1+2+3= 286
Retrocessos 11+1=12
75
Retrocesso
Testes 286+2+4= 292
Retrocessos 12
76
Retrocesso
Falha
6
Retrocede
5
Testes 292+1+3+2+5+3+1+2+3= 312
77
Retrocessos 12+1=13
Retrocesso
Falha
5
Retrocede
4e3
Testes 312+1+2+3+4= 322
Retrocessos 13+2=15
78
Retrocesso
X1=1
X2=3
X3=5
Impossível
Testes 322 + 2 = 324
Retrocessos 15
79
Propagação
Testes 0
Retrocessos 0
80
Propagação
Q1 #\= Q2,
1
L1+Q1 #\= L2+Q2,
L1+Q2 #\= L2+Q1.
1
1
1
1
1
1
1
Testes 8 * 7 = 56
1
1
1
1
1
1
Retrocessos 0
81
Propagação
1
1
1
2
1
2
1
2
1
1
2
1
2
1
2
1
2
Testes 56 + 6 * 6 = 92
2
1
2
1
2
1
2
1
Retrocessos 0
82
Propagação
1
1
1
2
1
2
1
2
1
1
2
3
2
1
2
3
2
3
1
2
3
1
2
3
1
2
1
2
3
1
3
Testes 92 + 4 * 5 = 112
1
Retrocessos 0
83
Propagação 2
X6 só pode
tomar o
valor 4
1
1
1
2
1
2
1
2
1
1
2
3
2
1
2
3
2
3
1
2
3
1
2
3
1
2
1
2
3
1
3
Testes 92 + 4 * 5 = 112
1
Retrocessos 0
84
Propagação 2
1
1
1
2
1
2
1
6
2
1
2
3
2
6
1
2
3
3
1
2
3
1
2
1
1
3
1
1
6
2
2
6
3
2
6
3
Testes 112+3+3+3+4 = 125
6
1
Retrocessos 0
85
Propagação 2
X8 só pode
tomar o
valor 7
1
1
1
2
1
2
1
6
2
1
2
3
2
6
1
2
3
3
1
2
3
1
2
1
1
3
1
1
Testes 125
6
2
2
6
3
2
2
3
6
1
Retrocessos 0
86
Propagação 2
1
1
1
2
1
2
1
6
2
1
2
3
2
6
1
2
3
3
1
2
3
1
2
1
1
3
1
1
Testes 125
6
2
2
6
3
2
2
3
6
1
Retrocessos 0
87
Propagação 2
1
1
1
2
1
2
1
6
2
1
2
3
8
2
6
1
2
3
3
1
2
3
1
2
1
1
3
1
1
6
2
2
6
3
8
2
2
3
6
Testes 125+2+2+2=131
1
Retrocessos 0
88
Propagação 2
X4 só pode
tomar o
valor 8
1
1
1
2
1
2
1
6
2
1
2
3
8
2
6
1
2
3
3
1
2
3
1
2
1
1
3
1
1
Testes 131
6
2
2
6
3
8
2
2
3
6
1
Retrocessos 0
89
Propagação 2
1
1
1
2
1
2
1
6
2
1
2
3
8
2
6
1
2
3
3
1
2
3
1
2
1
1
3
1
1
Testes 131
6
2
2
6
3
8
2
2
3
6
1
Retrocessos 0
90
Propagação 2
1
1
1
2
1
2
1
6
2
1
2
3
8
2
6
1
2
3
4
3
1
2
3
1
2
1
1
3
1
1
6
2
2
6
3
8
2
2
3
6
Testes 131+2+2=135
1
Retrocessos 0
91
Propagação 2
X5 só pode
tomar o
valor 2
1
1
1
2
1
2
1
6
2
1
2
3
8
2
6
1
2
3
4
3
1
2
3
1
2
1
1
3
1
1
Testes 135
6
2
2
6
3
8
2
2
3
6
1
Retrocessos 0
92
Propagação 2
1
1
1
2
1
2
1
6
2
1
2
3
8
2
6
1
2
3
4
3
1
2
3
1
2
1
1
3
1
1
Testes 135
6
2
2
6
3
8
2
2
3
6
1
Retrocessos 0
93
Propagação 2
1
1
1
2
1
2
1
6
2
1
2
3
8
2
6
1
2
3
4
3
1
2
3
1
2
1
1
3
2
1
5
2
6
3
8
1
6
2
2
3
6
Testes 135+1=136
1
Retrocessos 0
94
Propagação 2
1
1
1
2
1
2
1
6
2
1
2
3
8
2
6
1
2
3
4
3
1
2
3
1
2
1
1
3
2
1
5
2
6
3
8
1
6
2
2
3
6
Testes 136
1
Retrocessos 0
95
Propagação 2
1
1
Falha
1
2
1
2
7
1
6
2
1
2
3
8
Retrocede
1
2
6
1
2
3
4
3
1
2
3
1
2
3!
1
3
2
1
5
2
6
3
8
1
6
2
2
3
6
Testes 136
1
Retrocessos 0+1=1
96
Propagação 2
1
X1=1
X2=3
X3=5
Impossível
1
1
2
1
2
2
1
1
1
1
Testes 136
1
3
Testes
2
1
3
2
1
3
2
136
3
(324)
3
3
2
1
2
3
2
3
1
2
2
3
Retrocessos
1
(15)
1
Retrocessos 1
97
Propagação de Restrições
A programação deste tipo de mecanismo num sistema de
Programação em Lógica com Restrições segue o seguinte
esquema.
Problema ( Vars):Declaração de Variáveis e Domínios,
Lançamento das Restrições,
Enumeração das Variáveis.
Desta forma sempre que fôr enumerada uma variável, os
efeitos dessa enumeração são propagados automáticamente
para as restrições relevantes, diminuindo os domínios
possíveis para as outras variáveis.
Caso um domínio fique vazio, a pesquisa falha e é executado
o retrocesso.
98
Propagação de Restrições
Este é o estilo de programação adoptado no programa
rainhas_sat_1fd.
% Declaração de Domínios
domain([Q1,Q2,Q3,Q4,...,Q13,Q14,Q15,Q16],0,1)
% Lançamento de Restrições (1ª linha)
~Q1 # ~Q2, ~Q1 # ~Q3, ~Q2 # ~Q3,
~Q1 # ~Q4, ~Q2 # ~Q4, ~Q3 # ~Q4,
Q1 # Q2 # Q3 # Q4,
% Enumeração das Variáveis
labeling([], [Q1,Q2,Q3,Q4,...,Q13,Q14,Q15,Q16])
99
Propagação de Restrições
O lançamento de restrições é tratado de uma forma
semelhante à anterior, mas usando operadores de relação
específicos (antecedidos de #).
Desta forma, a avaliação tem em vista a redução do domínio
das variáveis.
X # Y :exp(X # Y, Exp), Exp #>= 1.
exp(X, X):- var(X), !.
exp(X, X):- atom(X), !.
exp(~X, Exp):- !, exp(X, ExpX), Exp #= 1-ExpX.
exp(X # Y, Exp):- !,
exp(X, ExpX), exp(Y, ExpY), Exp #= ExpX + ExpY.
100
Propagação de Restrições
Por exemplo,
X | ?- domain([X,Y], 0,1), X # Y.
X in 0..1,Y in 0..1 ? ; % não pode propagar
no
?- domain([X,Y], 0,1), X # Y, X #= 1.
X = 1,Y in 0..1 ? ;
% não pode propagar
no
?- domain([X,Y], 0,1), X # Y, X #= 0.
X = 0,Y = 1 ? ;
% propaga de X para Y
no
?- domain([X,Y], 0,1), X + Y #> 1.
X = 1,Y = 1 ? ;
% propaga para X e Y
no
101
Propagação de Restrições
Em geral a solução de um problema usando propagação de
restrições é bastante mais eficiente que a alternativa de
retrocesso puro.
A medição da eficiência pode ser feita pela invocação dos
predicados pré-definido fd_statistics/0 e fd_statistics/2
| ?- fd_statistics.
Resumptions: 28
Entailments: 2
Prunings: 23
Backtracks: 0
Constraints created: 4
yes
102
Propagação de Restrições
Para um problema tão pequeno como as 4 rainhas, as
diferenças na eficiência das duas versões não são
significativas.
No entanto tal não é o caso com instâncias maiores do
problema.
Esta diferença pode ser verificada na execução dos
programas
rainhas_sat_2bk
e
rainhas_sat_2fd
que são parametrizados pela dimensão do problema.
103
Domínios Finitos
Em muitas situações, e não obstante o interesse teórico e
prático do problema SAT, os problemas são mais
naturalmente especificados com variáveis cujo domínio não
se restringe aos valores 0/1, podendo tomar outros valores
(inteiros, no caso do SICStus).
Em particular, o problema das N rainhas é mais
naturalmente programado com N variáveis, uma para cada
linha, cujo valor denota a coluna que uma rainha deve
tomar nessa linha.
Esta especificação, não só é mais natural como pode
conduzir a uma substancial melhoria de eficiência.
104
Domínios Finitos
Com efeito, estas codificações representam um espaço de
pesquisa de dimensão substancialmente diferente.
Domínios Booleanos
k*n variáveis de valores 0/1.
Espaço de pesquisa = 2k*n.
Domínios Finitos
n variáveis de valores 1..k.
Espaço de pesquisa = kn = 2log2(k)*n
Razão dos espaços de pesquisa
r= 2k*n / 2log2(k)*n = 2 (k-log2(k))*n
Por exemplo, com k=8 e n=8, vem r=2(8-3)*8 =240
105
Domínios Finitos
Em geral, a variação do espaço a pesquisar não é tão
substancial, nomeadamente se existir uma propagação
eficiente no caso dos booleanos.
Por exemplo, no caso das rainhas pode garantir-se que só
uma em cada grupo de k variáveis (numa linha, coluna ou
diagonal) pode tomar o valor 1. Quando isto se verificar, a
propagação impõe que todas as outras tomem o valor 0, sem
escolha.
No entanto, as diferenças ainda são normalmente bastante
substanciais, como se pode ver nos exemplos codificados
directamente em domínios finitos
rainhas_bk
e rainhas_fd
106
Domínios Finitos
A eficiência das programas em domínios finitos (incluindo
booleanos) podem ainda ser melhoradas pelo uso de
•
Algoritmos de Propagação mais adequados
•
Heurísticas para escolha
•
da variável
•
do valor
Estas variações podem ser verificadas na versão do
programa das rainhas em domínios finitos
rainhas_fd
107