Algoritmo Chaff

Chaff é um algoritmo para resolver instâncias do Problema de satisfatibilidade booleana em programação. Ele foi desenvolvido por pesquisadores na Universidade de Princeton, Estados Unidos. O algoritmo trouxe melhorias de desempenho ao algoritmo DPLL (Davis-Putnam-Logemann-Loveland ) com um número de realces para uma implementação eficiente.No método Chaff, a parte principal não está baseada em algoritmos sofisticados para a redução do espaço de busca, mas em um desenho bastante eficiente em uma das etapas cruciais do método DPLL: a propagação unitária. É nessa fase que se mostra mais necessário os esforços de otimização.

Implementações editar

Algumas implementações disponíveis do algoritmo em software são mChaff, xChaff e zChaff, o último sendo o mais conhecido e usado, inclusive esta implementação já ganhou diversos concursos de resolvedores SAT. Chaff concentra-se em aperfeiçoar vários aspectos do algoritmo DPLL, seu bom desempenho é devido ao uso de Literais observados(vigiados), retrosaltos(backjumping), reinícios aleatórios e heurística para lidar com aprendizado. A seguir, o algoritmo zChaff mostrará o procedimento de forma semelhante à supracitada.

zChaff editar

A heurística Chaff tende a melhorar a técnica utilizada pela heurística SATO (SAtisﬁability Testing Optimized) utilizando literais observados. Em contraste com as listas Head and Tail(ver lista simplemente ligada) não há ordem entre os dois ponteiros. A falta de ordem tem a vantagem de que os literais não precisam ser atualizados quando são executados os backtrackings(re-leitura ou voltar atrás). Algumas extensões ao procedimento básico do Davis-Putnam foram bem sucedidas na heurística zChaff.

1.Algumas regras de poda foram incorporadas com sucesso em zChaff. A maioria dessas regras são variáveis de estado dependentes, isto é, são estatísticas de ocorrência de variáveis não-assinaladas usadas para marcar o banco de dados das cláusulas a fim de simplificar as variáveis já assinalada.
2.Em zChaff adota-se o processo de aprendizagem de conflitos (Conflict Learning) aplicado primeiramente em Relsat e posteriormente aprimorado em GRASP. Esse processo evita que o algoritmo no espaço futuro de procura encontre os mesmos conflitos já mapeados.
3.O backtracking não-cronológico discutido em GRASP é utilizado também nessa heurística com o objetivo de aprimorar o backtracking tradicional proposto por Davis-Putnam.
4.Após abortar a execução devido ao excesso de algum parâmetro, reinicializações (restarts) são presentes nesse algoritmo. Esse processo evita que o algoritmo SAT se perca em partes não-relevantes do espaço de procura. O processo de aprendizagem afeta o conceito de reinicializações em cláusulas novas durante duas reinicializações e então modifica o banco de dados das cláusulas.

Principais Funções editar

As principais funções relacionadas a tal heurística são:

1. decide-next-branch: Esta função implementa a regra de poda. Cada variável x mantém o contador de literais (literal count) para contar o número de ocorrências de x e de ¬x em cláusulas pertencentes ao banco de dados. São mantidos também as contagens (scores) para cada x e ¬x individualmente. Todas as variáveis são mantidas em ordem decrescente com a função maxscore(x) = max(score(x),score(¬x)) usada para ordenar a relação. Diante da aprendizagem de conflitos, o contador de literais pode ser aumentado e atualizações sempre são realizadas. Seja x variável, scoreold(x),scoreold(¬x) são as atuais contagens e seja increase(x),increase(¬x) o incremento de x e ¬x desde a última atualização. Logo a nova contagem é realizada como:

       scorenew(x) = scoreold(x)/2 + increase(x)
       scorenew(¬x) = scoreold(¬x)/2 + increase(¬x)

Para uma nova ramificação de variáveis e um novo assinalamento das variáveis, a variável x com o valor máximo maxscore(x) é selecionado e seu assinalamento x = 1 se score(x) ≥ score(¬x) e x = 0 se score(x) < score(¬x). Já que a contagem de literais somente é aumentada quando uma cláusula conflitante no banco de dados é adicionada, essa regra ocorre em cláusulas conflitantes aprendidas. Além disso, há contagem de variáveis que nunca ocorrem ou raramente ocorrem nas cláusulas conflitantes se dividida por dois.

2. deduce: Essa função incorpora a regra de propagação unitária (unit propagation rule) de uma maneira repetida e é chamada de BCP (boolean constraint propagation). A função principal do deduce é deduzir uma implicação de uma fila de implicações e checar todas as cláusulas não-satisfeitas se elas são agora satisfeitas ou se tornaram cláusulas unitárias a partir dessa nova implicação. Além disso, essa implicação e assinalada no nível de decisão nomeada no assinalamento anterior da decisão. Todos os assinalamentos de implicações para um nível de decisão são armazenados numa lista de anexada. Se um conflito ocorre, ou seja, uma cláusula é identificada como não-resolvida, todas as cláusulas não-resolvidas são coletadas para permitir que a análise de conflitos baseada em cláusulas não-resolvidas. A função retorna NO-CONFLICT se nenhum conflito ocorre e retorna CONFLICT se ocorre conflito.

3. analyze-conflicts: Essa função ocorre dentro da função deduce. Um conflito ocorre quando um assinalamento contraditório na variável é deduzido. Por exemplo, seja x uma variável que já tenha sido assinalada com o valor x = 1 e a partir da função deduce encontramos o valor x = 0 o que caracteriza um conflito. Se c = x temos que c é uma cláusula conflitante. A partir do aprendizado através da cláusula conflitante o nível de backtracking é computado.

4. backtrack: Depois da análise de conflitos é necessário realizar um backtrack num certo nível b de decisão (para um melhor entendimento sobre o nível de decisão, ver exemplo no final do artigo) computado pela função analyze-conflicts. Logo todas as implicações e decisões de assinalamentos com nível de decisão r ≥ b são recompostas. Se dentro de uma cláusula conflitante c somente um literal tiver seu nível de decisão, este literal é diretamente implicado. Esta implicação pode disparar novas implicações pela função deduce.

Acima, as funções principais do zChaff.

Literais Observados editar

Um dos principais avanços propostos, primeiramente por Chaff, e posteriormente incorporado em zChaff é o que chamamos de literais observados (watched literals). Na prática, para a maioria dos problemas SAT, mais que 90% no tempo de execução de um resolvedor é responsável pelo processo BCP. Logo um eficiente BCP é de fundamental importância para a sua implementação, deseja-se achar uma forma rápida de visitar todas as cláusulas que se tornaram novas implicações por uma simples adição ao conjunto de assinalamentos. A forma mais intuitiva é simplesmente olhar cada cláusula no banco de dados que está assinalada para 0. Deve-se ter um contador para cada cláusula que tenha o valor 0 e modificá-lo toda vez que um literal da cláusula for mudado para 0. Com esse objetivo, pode-se escolher dois literais não assinalados para 0 em cada cláusula para observar a qualquer momento. Então pode-se garantir que até que um desses dois literais sejam assinalados para 0, não se pode ter mais que N −2 literais que na cláusula assinalados para 0 o que torna a cláusula não implicada.

Ao se visitar uma cláusula temos:

1. A cláusula não é implicada, então pelo menos dois literais não estão assinalados para 0, incluindo o outro literal observado corrente. Isto significa que pelo menos um literal não-observado não está assinalado para 0. Escolhe-se então este literal para substituir o que está assinalado para 0. Se mantém a propriedade que dois literais observados não estão assinalados para 0.

2. A cláusula é implicada então deve-se notar que a variável implicada deve ser o outro literal observado, já que pela definição, a cláusula tem somente um literal não assinalado para 0, e um dos dois literais observados é agora assinalado para 0.

Podemos observar na Figura abaixo o funcionamento do BCP de zChaff através de dois literais observados.

Dois Literais Observados.

A Figura acima mostra como os literais observados de zChaff para uma cláusula simples muda de acordo com o assinalamento de suas variáveis. Observe que a escolha inicial dos literais observados é arbitrária. O BCP em SATO é bem parecido com o apresentado em zChaff. A diferença básica entre zChaff e SATO é o fato de que em zChaff não é necessário o deslocamento numa direção fixa para os literais observados. Em SATO o head só pode movimentar-se em direção ao tail e vice-versa. Na Figura acima observamos que o os literais observados estão, a princípio, apontados para o início e fim da cláusula (o que não é necessário em zChaff). Porém, à medida que é executado o procedimento, não há mais direção fixa, como aconteceria em SATO.

Resolvente editar

O principal avanço de zChaff é a criação do que chamaremos resolvente com o intuito de prevenir erros no decorrer da heurística. Seja a FNC $(x_{1}\lor x_{2})\land (\neg x_{2}\lor x_{3})$ . Essa fórmula é equivalente a $(x_{1}\lor x_{2})\land (\neg x_{2}\lor x_{3})\land (x_{1}\lor x_{3})$ (pode ser verificado utilizando tabela verdade). O resolvente - definido como uma tautologia que podemos extrair de determinada fórmula - da fórmula $(x_{1}\lor x_{2})\land (\neg x_{2}\lor x_{3})$ será dado por $\ (x_{1}\lor x_{3})$ já que temos a implicação $(x_{1}\lor x_{2})\land (\neg x_{2}\lor x_{3})\to (x_{1}\lor x_{3})$ .

Por exemplo, seja $F=(a\lor b)\land (\neg a\lor \neg b\lor \neg c)\land (\neg b\lor c)$ e se tomarmos $\ a=1$ não é executado o processo de dedução (já que na parte restante $(\neg a\lor \neg b\lor \neg c)\land (\neg b\lor c)$ não se pode extrair nenhum resolvente). Quando $\ b=1$ ocorre um conflito entre $(\neg a\lor \neg b\lor \neg c)$ e $(\neg b\lor c)$ . O resolvente será dado por $(\neg a\lor \neg b)$ o que evitará problemas futuros.

A verificação da veracidade dos resolventes se faz por meio do uso de tabelas verdades já que as fórmulas descritas em cada exemplo são equivalentes. Esta “descoberta” de equivalência se que torna zChaff uma heurística mais poderosa que as anteriores.

Exemplo editar

zChaff incorporou os avanços da heurística GRASP e SATO o que significa que a forma de se tratar conflitos (usando Grafos de Implicação) e o uso do backtracking não-cronológico são utilizados nesta heurística além da ideia de literais observados. A grande diferença que determinou uma melhoria em zChaff foi a utilização dos ponteiros que podem se mover livremente e, inicialmente, podem apontar para qualquer variável da cláusula. Seja a seguinte cláusula num nível de decisão n qualquer (Figura abaixo, da estrutura de zChaff):

\left(\lnot x_{1}\lor x_{4}\lor \lnot x_{7}\lor x_{12}\lor x_{15}\right)

Sabemos que há dois ponteiros podendo apontar $\ x_{7}$ e para $\ x_{12}$ . Seja $\ x_{1}=1$ @ $\ 1$ (<valor da variável>@<nível de decisão>), logo os ponteiros não mudam de posição. Seja $\ x_{7}=1$ @ $\ 2$ e $\ x_{15}=0$ @ $\ 2$ então um ponteiro aponta para $\ x_{4}$ (em zChaff os ponteiros se movem livremente) e o outro não muda de posição. Seja $\ x_{4}=0$ @ $\ 3$ implicando que $\ x_{12}$ assuma o valor 1, tornando a cláusula satisfeita. Entretanto, suponha que no banco de dados das variáveis, $\ x_{12}$ gera um conflito, então um backtracking é executado ao nível de decisão 1 (nível inicial de acordo com o exemplo), apagando todas as decisões posteriores a este nível. A configuração atual é um ponteiro apontando para $\ x_{4}$ e outro apontando para $\ x_{12}$ já que quando é executado um backtracking em zChaff não é necessário refazer o apontamento inicial dos ponteiros. Seja $\ x_{12}=1$ @ $\ 2$ e $\ x_{7}=0$ @ $\ 2$ , temos então que a cláusula assume o valor 1 e não é mais visitada. Em zChaff, encontrando uma atribuição que faz com que a cláusula seja 1, os ponteiros se movem também (diferentemente de SATO).