Essa subseção apresenta os resultados, em uma versão inicial, do algoritmo descrito na Figura 4.4. O objetivo e a razão da inserção desses resultados é simplesmente avaliar o desempenho prático da subtração de cubos em instâncias do problema SAT. Na verdade, as instâncias de teste utilizadas são relativamente simples, mas nos permitem uma comparação do desempenho entre um solucionador baseado na operação DSharp e o DPLL.
A estrutura de dados utilizada foi basicamente a mesma para os dois solucionadores: uma lista de adjacências conforme descrito no capítulo 3.
Para o solucionador DPLL:
• Para cada cláusula, existe uma lista de literais e a quantidade de literais avaliados como verdadeiros ou falsos;
• Para cada variável, existe uma lista de cláusulas onde ela aparece, o valor atual atribuído à mesma (verdadeiro, falso ou livre), o nível da árvore de decisão onde esta atribuição foi realizada e uma variável de controle identificando se a variável já foi avaliada nas suas duas fases;
• O algoritmo DPLL adotado é o mesmo descrito no capítulo 3. Como se trata de um procedimento não recursivo, existe uma pilha das atribuições para o retro- cesso.
Para o solucionador DSharp:
• Para cada cláusula-cubo, existe de uma lista de variáveis, representadas por um valor numérico identificando a variável e outra para o seu valor especificado. Apenas estão presentes na lista as variáveis especificadas, se uma variável é não especificada (ou possui o valor X), ela não aparece na lista da cláusula-cubo; • Como o procedimento é recursivo, a pilha, com as atribuições de cada nível, está
implicitamente determinada. A cada chamada recursiva, caminhamos dentro da lista da cláusula-cubo identificando a próxima variável a ser subtraída. Isso nos permite um caminhamento em profundidade (DFS ) na árvore de decisões DSharp;
• O cubo resposta inicial é representado por uma lista vazia, todas as variáveis são não especificadas, a cada operação DSharp, as variáveis que recebem alguma atribuição, se tornam especificadas, são inseridas nessa lista.
Nenhuma heurística foi implementada em nenhum solucionador, isto é, para o solu- cionador DPLL, não existe uma heurística de decisão, as variáveis e os valores atribuídos a cada decisão são aleatoriamente escolhidos e o retrocesso é cronológico. Para o so- lucionador baseado no DSharp, as cláusulas-cubo são aleatoriamente escolhidas, todas as operações entre os cubos são realizadas e os mecanismos de cobertura ou interseção nula não são avaliados.
As instâncias utilizadas foram obtidas do pacote de instâncias do DIMACS [Url13] e obtidas em [Url18]. O grupo de instâncias consiste no pacote de instâncias AIM. As instâncias AIM, elaboradas por Iwama, Miyano e Asahiro em [Aim96], foram elabora- das através de um gerador aleatório de instâncias 3-SAT. O gerador trabalha de forma completamente aleatória o que diferencia as instâncias geradas daquelas que utilizam uma geração com um certo determinismo ou daquelas instâncias que são traduções de problemas. O pacote de instâncias inclui:
• Instâncias não-SAT com relações cláusulas/variáveis baixos
• Instâncias SAT com relações altas e baixas, mas que possuem apenas uma atri- buição de variáveis que torne a instância SAT.
As instâncias são identificadas como aim-xxx-y_y-zzzz-j, onde:
• Todos os nomes possuem "aim"no início (referente às iniciais Asahiro, Iwama e Miyano)
• xxx mostra o número de variáveis 50, 100 ou 200
• y_y mostra a relação cláusulas/variáveis (1.6, 2.0, 3.4 ou 6.0)
• zzzz significa "no"ou "yes1 ", o primeiro denota a não existência de um conjunto de atribuições e o segundo que existe apenas uma atribuição de variáveis que torne o problema satisfazível
• o último j indica apenas qual j-ésima instância dentro daquele grupo.
A razão para escolha desse conjunto de instâncias é que os solucionadores são relati- vamente simples e o tempo necessário para chegarmos a uma resposta, nesse conjunto de instâncias, é relativamente baixo. Para as simulações, foi adotado um tempo limite de 1000 segundos, ou seja, o solucionador tem este tempo limite para encontrar uma atribuição para as variáveis que torne a instância proposta satisfazível ou indicar que a
instância não é satisfazível. Se pacotes de instâncias mais complexas forem utilizados, um número grande de instâncias do conjunto romperá o tempo limite para ambos os solucionadores, prejudicando a análise dos resultados. O objetivo, no momento, é uma análise relativa entre dois solucionadores e não uma análise absoluta do desempenho de um solucionador.
Os solucionadores foram executados em um computador Pentium 4, com uma freqüência de 2.0 GHz e 1GByte de memória. O sistema operacional utilizado foi o Linux. Os resultados estão apresentados na Tabela 4.2. Na tabela, cada linha repre- senta a instância avaliada e as colunas mostram: o número de variáveis da instância (Var.), o número de cláusulas (Clá.), se a instância é SAT ou não-SAT (sat) e o tempo em segundos gasto pelo solucionador. Foi utilizado o termo TO (time out), se o tempo necessário para chegarmos a uma resposta foi superior ao tempo limite. Para o so- lucionador DSharp, temos uma coluna indicando o número de subtrações realizadas e para o solucionador DPLL uma coluna indicando o número de decisões realizadas. Para as instâncias onde o solucionador DSharp é mais rápido, o tempo de solução está em negrito.
O que podemos observar dos resultados é que existe uma nítida vantagem do pro- cesso de subtração de cubos sobre o DPLL clássico. Além de apresentar um tempo de solução inferior, o solucionador é mais robusto dentro do tempo limite especificado. Se desconsiderarmos as instâncias onde um, ou ambos, apresentaram um tempo superior ao tempo limite, o solucionador DSharp se mostra 3,57 vezes mais veloz que o DPLL. Apesar de encontrarmos instâncias onde este ganho é superior a 1000 vezes. Aparen- temente não se pode correlacionar a melhoria obtida com o fato da instância ser SAT ou não-SAT e nem com a relação cláusulas/variáveis.
Um grande problema encontrado e que tornou o solucionador DSharp lento, foi a estrutura de dados utilizada para a representação dos cubos. Tendo em mente que, a cada subtração realizada, no mínimo um elemento, ou uma variável especificada, é inserida no cubo resposta, de acordo com a implementação utilizada, isso significou
percorrer a lista de variáveis para a inserção desse elemento. Esse fato tornou o tempo de resposta do solucionador dependente do tamanho da lista e, de uma forma mais cruel, da quantidade de subtrações. Essa característica é a principal desvantagem da estrutura de dados utilizada e que, fatalmente, inviabiliza a sua implementação. Mas, mesmo com essa estrutura de dados inadequada, o solucionador se mostra competitivo frente ao DPLL.