De forma a perceber a intuição sobre o solucionador SAT DSharp, um exemplo sim- ples com uma descrição similar ao algoritmo DPLL clássico será utilizada, ou seja, nenhuma das técnicas atualmente sobrepostas ao DPLL original, tais como retrocessos não cronológicos, aprendizado de cláusulas e reinicializações, serão inseridas ao solu- cionador. Posteriormente algumas técnicas de simplificação, análogas a estas técnicas, serão exibidas.
Para uma fórmula φ = w1∧ w2∧ . . . ∧ wm na FNC, inicialmente negamos ambos os
lados e obtemos: ¬φ = ¬w1∨ ¬w2∨ . . . ∨ ¬wm, e que, conforme vimos, corresponde ao
conjunto de cláusulas-cubo cc(φ) = c1c2. . . cm . A disjunção das cláusulas-cubo repre-
senta todas as regiões do espaço de procura onde não encontraremos uma atribuição das variáveis capaz de satisfazer a instância φ do problema SAT.
Iniciando com um cubo universal u = (u1u2. . . um), que denota todo o espaço de
procura e onde cada elemento ui possui o valor X, ao sucessivamente aplicarmos a
operação DSharp entre o atual espaço de procura e cada cláusula-cubo, chegaremos ao subespaço solução da instância φ se ela for satisfazível, ou a um subespaço vazio, se ela
não for. O conjunto de cubos solução Sφ é dado por:
Sφ= (((((u#c1)#c2) . . .)#cm)
Após cada operação DSharp obtemos um conjunto de subespaços de procura disjuntos. As cláusulas-cubo restantes devem ser subtraídas de cada um desses subespaços. A escolha da subtração disjunta evita que a procura seja realizada de forma repetida em cada subespaço.
O algoritmo básico de um solucionador SAT DSharp é ilustrado a seguir. O so- lucionador é definido de forma recursiva e é inicialmente chamado a partir da rotina principal, passando como argumentos u = (XX . . . X) como o atual espaço de procura e o nível como 0, ou nível inicial. O pseudocódigo está descrito na Figura 4.4.
A função Decide( ) é responsável por escolher o próximo cubo a ser subtraído, nenhuma heurística será utilizada nesta etapa, todas as cláusulas-cubo são igualmente tratadas e aleatoriamente escolhidas.
A função Dsharp ( ) executa a operação DSharp entre o espaço corrente de procura e a cláusula-cubo eleita pela função Decide( ). Ela executa exatamente a operação descrita na Definição 1.
Soluciona (solução_corrente, nível) inicio
se (nível = último nível)
retorne (SAT);
clausula_cubo_escolhida = Decide ( );
C=Dsharp (solução_corrente, cláusula_cubo_escolhida);
para ( cada cubo ci em C )
retorno_solucionador = Soluciona(ci, nível +1); se (retorno_solucionador = SAT)
retorne (SAT);
fimpara
retorne ( não_SAT);
fim
Figura 4.4: Pseudo código do solucionador SAT baseado em DSharp
Como em um solucionador baseado em DPLL, existem algumas estratégias para se chegar mais rapidamente à resposta SAT ou não-SAT para uma instância:
• Um conflito é alcançado quando uma cláusula-cubo a ser subtraída, cobre o espaço de procura corrente, nessa situação acontece um retrocesso. A justificativa é simples, essa situação significa que o espaço booleano da cláusula-cubo é maior do que o espaço onde estamos buscando a solução, assim sendo, devemos sair deste espaço imediatamente;
• Se uma cláusula-cubo possui uma interseção nula com o espaço corrente de pro- cura, não existe a necessidade de se aplicar a operação DSharp, o resultado é o próprio espaço de procura. A justificativa é que esta restrição, ou a cláusula cubo,
não se aplica ao espaço onde estamos procurando a solução, conseqüentemente não existe a necessidade de se executar a operação DSharp, mesmo porque o re- sultado de se aplicar o operador seria o próprio espaço corrente, esta simplificação nos permite deixar de executar uma operação DSharp;
• Finalmente, uma implicação (ou a propagação de restrição booleana-BCP) acon- tece, quando a operação DSharp produz apenas um cubo como resultado. O algoritmo pode se melhor entendido através de um exemplo contendo uma fórmula simples codificada em CNF:
φ = (¬x1∨ x2∨ ¬x4) ∧ (x1 ∨ ¬x2∨ x3) ∧ (x1∨ ¬x3∨ ¬x4)
Invertendo, iremos obter:
¬φ = (x1∧ ¬x2∧ x4) ∨ (¬x1∧ x2∧ ¬x3) ∨ (¬x1∧ x3∧ x4)
Em uma notação de cubos temos:
cc(φ) = {(10X1), (010X), (0X11)}
Iniciando-se com u = (XXXX), o que representa a atribuição de um valor não especi- ficado para x1, x2 , x3 e x4, tomamos aleatoriamente a primeira cláusula-cubo a ser sub-
traída e, aplicando o algoritmo DSharp, obtemos como resposta: (XXXX)#(10X1) = {(0XXX), (11XX), (10X0)}, que representa três subespaços disjuntos de procura.
A partir desse ponto, podemos realizar a procura através de uma busca em largura (BFS) ou uma busca em profundidade (DFS). Se tomarmos a segunda cláusula cubo para subtrair, temos os seguintes resultados:
(0XXX)#(010X) = {(000X), (011X)}, (11XX)#(010X) = {(11XX)} e
Observa-se que as duas subtrações finais foram desnecessárias, o espaço de procura após a subtração foi idêntico ao espaço de procura anterior à subtração, já que a interseção entre ambos é nula. E finalmente, subtraindo a terceira cláusula-cubo: (000X)#(0X11) = {(000X)(0010)},
(011X)#(0X11) = {(0110)}, (11XX)#(0X11) = {(11XX)} e (10X0)#(0X11) = {(10X0)}.
O resultado final é Sφ = {(000X), (0010), (0110), (11XX), (10X0)}, onde temos
todas as atribuições às variáveis que tornam a instância satisfazível, apresentadas de forma disjunta.
O ponto fundamental a observar é que, como todos esses subespaços respostas de subtrações possuem interseção nula, evita-se uma busca desnecessária em regiões de procura sobrepostas, o que representa a principal justificativa para o uso da operação DSharp. A busca em regiões que se sobrepõem significa a aplicação desnecessária do operador e, conseqüentemente, em mais tempo para se chegar a uma resposta.
A árvore completa de procura, para o exemplo ilustrado, pode ser vista na Figura 4.5. Cada nível da árvore corresponde à operação DSharp entre o subespaço corrente de procura e uma cláusula-cubo, neste exemplo, na mesma ordem em que elas aparecem na fórmula original.
Observa-se que a implementação simples desse algoritmo rapidamente poderia con- sumir recursos de memória para fórmulas grandes, já que um grande número de cláu- sulas cubo iria proliferar após cada operação DSharp. Conclui-se que uma busca em largura (BFS ) é ineficiente. Uma abordagem mais eficiente, em termos de memória, seria uma busca em profundidade (DFS ), subtraindo o cubo seguinte apenas do cubo disjunto previamente obtido pela operação # anterior. Estas duas direções de procura estão indicadas na Figura 4.5.
ø ø ø ø ø ø ø ø ø ø ø ø ø ø ø ø ø 000X 011X ø 11XX 10X0 0010 000X 0110 11XX 10X0 11XX 10X0 0XXX XXXX ø ø (¬x x ¬x )1 2 4 (x ¬x x )1 2 3 ( x ¬x ¬x )1 3 4 φ Instância SAT: = S = ( ( ( XXXX # 10X1) # 010X ) # 0X11 )φ BFS DFS #10X1 #010X #010X #010X #0X11 #0X11 #0X11 #0X11
Figura 4.5: Instância de um problema SAT e árvore de procura completa DSharp