Algoritmos de SAT

Os algoritmos de SAT (do inglês satisfiability) têm como propósito determinar se uma fbf é satisfazível e, em caso afirmativo, devolver uma interpretação que a satisfaça - um modelo dessa fbf, portanto. Os algoritmos de SAT são mais eficientes que OBDDs, visto que estes últimos dão-nos todos os modelos da fbf, o que pode ser bastante ineficiente (e neste caso não precisamos de todos os modelos). De recordar, ainda, que o facto de saber se uma fbf é satisfazível ou não é uma das questões fundamentais na Lógica, isto é, saber se uma fbf é consequência semântica de um conjunto de fbfs.

Vamos abordar 2 algoritmos de SAT:

  • um primeiro, baseado em propagação de marcas, muito eficiente mas incompleto, podendo terminar sem resposta.

  • um outro, algoritmo DP (nomeado em honra de Davis e Putman), que apesar de menos eficiente é completo.

Algoritmo baseado em propagação de marcas

A ideia por detrás deste algoritmo é, dada uma fbf, determinar as restrições que têm de ser satisfeitas pelas suas "sub-fórmulas" de modo a que a fbf seja verdadeira. Aqui, o conceito de subfórmula é, de um modo abstrato, como o de símbolo de proposição - "que valor é que cada um destes símbolos de proposição tem de ter para a fbf ser verdadeira". Por exemplo, para a fbf PQP \wedge Q ser satisfazível, tanto PP como QQ, as subfórmulas de PQP \wedge Q, têm de ter valor lógico verdadeiro (ou seja a interpretação pretendida tem de ser tal que I(P)=VI(P) = V e I(Q)=VI(Q) = V).

Ora, a noção de marca advém precisamente desta ideia: sempre que descobrimos que, para a fbf fazer sentido, uma dada subfórmula tem de ter um valor lógico concreto, marcamos essa subfórmula com esse valor lógico.

CHEGAR AOS DAG'S

Aqui, trabalhamos com grafos dirigidos e acíclicos, vulgo DAGs, grafos estes que vão corresponder às fbfs cuja satisfazibilidade vamos procurar provar. Chegamos a este grafo através de:

  • transformar a fbf original numa fbf que só contém conjunções e negações, recorrendo às regras usuais:

    • PQ¬(¬P¬Q)P \vee Q \leftrightarrow \neg(\neg P \wedge \neg Q)

    • PQ¬(P¬Q)P \to Q \leftrightarrow \neg(P \wedge \neg Q)

    • ¬¬PP\neg \neg P \leftrightarrow P (não obrigatório, contudo usualmente realizada no decorrer destes algoritmos)

    Por exemplo, simplificar ¬¬(P¬¬(¬PQ))\neg \neg (P \wedge \neg \neg (\neg P \vee Q)) resultaria sucessivamente em P(¬PQ)P \wedge (\neg P \vee Q), via eliminação da dupla negação, e P¬(P¬Q)P \wedge \neg (P \wedge \neg Q), via a primeira equivalência referida acima.

  • já com a fbf transformada nesta versão mais simplificada, podemos construir o nosso DAG:

    • uma fbf atómica, ou seja um símbolo de proposição, é uma árvore que é constituída apenas pela raiz, cujo rótulo é esse mesmo símbolo de proposição;

    • a negação, ¬P\neg P, é uma árvore cuja raiz é um nó de rótulo ¬\neg, do qual sai um caminho/arco que leva à raiz de uma árvore, raiz essa rotulada com PP.

    • a conjunção, PQP \wedge Q, é uma árvore de rótulo \wedge da qual saem dois caminhos/arcos, um para cada árvore cuja raiz é o respetivo símbolo de proposição.

Ora, este processo é sucessivamente aplicado até termos a árvore da fbf, cujas folhas são precisamente os símbolos de proposição que ocorrem na fbf. Para obter o DAG basta, agora, juntar as folhas com rótulos repetidos. Para ser ainda mais eficientes, podemos ainda partilhar nós repetidos (mas no livro não o fazem, nem nas aulas).

Faz agora sentido introduzir o DAG correspondente a (P¬(P¬Q))(P \wedge \neg (P \wedge \neg Q)):

À esquerda temos a primeira fase do processo, onde temos a raiz "principal" com rótulo \wedge, com arcos para PP e para o "lado" de ¬(P¬Q)\neg (P \wedge \neg Q). Ora, neste último, temos que a árvore tem raiz com rótulo ¬\neg, que terá caminho para P¬QP \wedge \neg Q. Aqui, voltamos a pegar no operador \wedge, fazendo dele a raiz e criando um caminho para PP e para ¬Q\neg Q. Resta ainda terminar o caminho de ¬Q\neg Q, criando uma árvore com raiz de rótulo ¬\neg com arco para QQ. Temos, portanto, a árvore terminada (à esquerda).

Por fim, juntamos as folhas com rótulos repetidos - neste caso, folhas com rótulo PP, tendo como resultado final o DAG à direita.

Propagação de marcas pelo grafo

Chegámos agora à próxima fase do algoritmo, a propagação de marcas (VV ou FF) pelo grafo. O primeiro passo é sempre marcar a raiz com VV. As seguintes marcas são dadas por um conjunto de regras:

  • Tendo um nó de rótulo ¬\neg marcado, o algoritmo propaga a marca "contrária" para os seus arcos; podemos ainda analisar o processo ao contrário - se temos um nó com rótulo marcado com arco "para cima" que leva a uma raiz com rótulo ¬\neg, então, a raiz com ¬\neg tem a marca oposta.

  • Tendo um nó de raiz \wedge marcada com VV, a marca VV é também propagada pelos respetivos arcos; podemos também fazer o processo inverso - se dois nós com marca VV tiverem arcos para o mesmo nó com rótulo \wedge, esse nó tem marca VV. Por outro lado, basta um dos nós ter FF para a conjunção ser falsa. Além disso, se um dos nós tiver marca VV mas a raiz tiver marca FF, podemos admitir que o outro nó tem marca FF.

Se repararem, acima foi mencionado algumas vezes o "processo inverso/ascendente" - isto porque, caso apenas ocorra a propagação de marcas no sentido descendente, temos de verificar, começando nas folhas, se a propagação inversa também faz sentido (e é igual à descendente). Se for, encontrámos uma interpretação que satisfaz a fbf; caso contrário, a fbf não é satisfazível.

Exemplos - Propagação de Marcas

A propagação de marcas relativas à fbf P¬(P¬Q)P \wedge \neg (P \wedge \neg Q) tem um aspeto deste género:

Se tentarmos realizar a propagação de marcas no sentido ascendente obtemos as mesmas marcas que no sentido descendente, pelo que a fbf é provada satisfazível, e encontrámos uma testemunha, interpretação que satisfaz a fbf. Contudo, talvez a explicação deste exemplo não seja suficiente para que esta verificação faça sentido - porque é que a propagação havia de ser diferente em sentidos diferentes? Bem, vejamos o exemplo abaixo, da fbf (P¬(P¬Q))¬Q(P \wedge \neg (P \wedge \neg Q))\wedge \neg Q:

Aqui, a propagação no sentido ascendente leva a marcas diferentes das propagadas no sentido descendente, pelo que a fbf não é satisfazível. Podemos ver isso tendo que, olhando para a raiz, é uma conjunção, pelo que ambas as raízes com arcos ligados pela conjunção terão marca VV, ficando com QQ assim propagado como FF, por via da negação ser verdadeira. Contudo, e olhando para o outro lado do DAG, temos que a nova conjunção também tem marca VV, pelo que tanto PP como a negação vão ser VV. A conjunção que segue a negação é falsa, portanto, mas tendo que PP é verdadeira a negação à direita tem de ser falsa (para a conjunção ser falsa) - sendo a negação falsa, QQ teria de ser verdadeira. Temos aqui um problema - logo no início marcámos QQ como falsa, e agora marcámo-la como verdadeira? Não pode ser, é uma contradição! Assim sendo, a fbf é obrigatoriamente contraditória, e portanto não satisfazível.

Foi referido acima que o algoritmo de propagação de marcas não é completo, isto é, podemos não conseguir atribuir marcas a todos os nós do grafo. Ora vejamos o exemplo de (PQ)(P¬Q)(PR)(P \to Q) \wedge (P \to \neg Q) \wedge (P \vee R):

Como podemos observar, ocorre (mais que uma vez até) chegarmos a situações em que a conjunção é falsa, mas não temos informação concreta sobre os "filhos", impossibilitando-nos portanto de aferir a marca de alguns símbolos de proposição. O resultado é, portanto, inconclusivo.

Para nos ajudar (até um certo ponto) a marcar mais algumas marcas que restem temos o algoritmo de testes de nós.

Algoritmo de testes de nós

Este algoritmo recebe um nó e um grafo. Marca temporariamente esse nó com VV e verifica se a propagação de marcas origina agora outras marcas consistentes - não contraditórias, portanto. Caso aconteça, fantástico, encontrámos uma testemunha da fbf com marcas corretas. Caso ocorra uma contradição, marcamos o nó que estávamos a testar com FF (permanentemente), removemos as marcas temporárias que criámos a testar este nó e testamos outro nó. Caso não ocorra uma contradição mas ainda fiquem nós por marcar, apagamos as marcas temporárias e voltamos a testar o mesmo nó, desta vez com a marca FF. Caso nenhum dos testes seja conclusivo, não havendo contradição mas restando ainda marcas por propagar, fazemos a interseção das marcas temporárias em comum entre os dois testes e marcamo-las permanentemente, procurando agora testar um nó diferente.

Ora, peguemos na fbf do último exemplo, (PQ)(P¬Q)(PR)(P \to Q) \wedge (P \to \neg Q) \wedge (P \vee R):

Aqui, testamos marcar PP com VV. Ora, do exemplo anterior, tínhamos que ambas as conjunções a que estava ligado eram falsas, o que levaria a que, simultaneamente, QQ e ¬Q\neg Q fossem falsas, o que é claramente contraditório. Marcamos, portanto, PP permanentemente com FF. Ora, com esta marca permanente podemos aferir alguns resultados, via propagação de marcas:

Falta apenas marcar QQ, mas aqui qualquer rotulação gera uma fbf satisfazível.

Resta, por fim, notar que este algoritmo continua a não ser completo - continua a haver casos em que, mesmo suportados pelo algoritmo do teste de nós, não conseguimos resolver todos os casos.

A grande vantagem destes algoritmos em relação aos algoritmos de DP é em relação à sua eficiência. O algoritmo de propagação de marcas tem crescimento linear, o de teste de nós cúbico, ambos substancialmente melhores que algoritmos baseados em DP que têm crescimento exponencial. É, portanto, uma questão de "pick your poison" - privilegiamos a eficiência ou a completude dos resultados?

Algoritmos baseados em DP

Utilizam regras que transformam conjuntos de cláusulas em outros conjuntos de cláusulas. Têm como principal vantagem em relação ao algoritmo estudado acima o facto de serem completos, terminando sempre com uma resposta. São, contudo, menos eficientes, apresentando crescimento exponencial.

Algoritmos baseados em DP

Sendo Δ\Delta um conjunto de cláusulas e PiP_{i} um símbolo de proposição, o conjunto de cláusulas obtido de Δ\Delta por eliminação de PiP_{i}, Pi(Δ)\exists P_{i} (\Delta), é obtido tal que:

  • Todos os resolventes-PiP_{i}, gerados a partir de cláusulas de Δ\Delta, são adicionados.

  • Todas as cláusulas de Δ\Delta que mencionam PiP_{i} são retiradas.

Tendo que nos resolventes obrigatoriamente não aparece PiP_{i} e que já não temos em consideração as cláusulas de Δ\Delta que mencionam PiP_{i}, nenhuma cláusula do conjunto Pi(Δ)\exists P_{i} (\Delta) mencionará PiP_{i}.

Como exemplo, podemos olhar para Δ={{P,Q},{¬P,Q},{¬P,S},{¬Q,R}}\Delta = \{\{P, Q\}, \{\neg P, Q\}, \{\neg P, S\}, \{\neg Q, R\}\}. Os resolventes-PP são {Q}\{Q\} e {Q,S}\{Q, S\}. Ignorando as cláusulas de Δ\Delta que mencionam PP, podemos então construir P(Δ)={{Q},{Q,S},{¬Q,R}}\exists P(\Delta) = \{\{Q\}, \{Q, S\}, \{\neg Q, R\}\}.

O algoritmo DP baseia-se no facto de Δ\Delta ser satisfazível se e só se Pi(Δ)\exists P_{i}(\Delta) é satisfazível (a demonstração, que ainda é comprida, encontra-se no livro que acompanha a cadeira).

Assim sendo, e pegando no exemplo utilizado na definição acima, podemos afirmar que Δ={{P,Q},{¬P,Q},{¬P,S},{¬Q,R}}\Delta = \{\{P, Q\}, \{\neg P, Q\}, \{\neg P, S\}, \{\neg Q, R\}\} só é satisfazível caso P(Δ)={{Q},{Q,S},{¬Q,R}}\exists P(\Delta) = \{\{Q\}, \{Q, S\}, \{\neg Q, R\}\} for satisfazível.

O algoritmo consiste em, partindo de uma fbf Δ\Delta já na forma clausal, ir eliminado sucessivamente os símbolos de proposição de Δ\Delta; desta forma, os conjuntos de cláusulas vão contendo cada vez menos símbolos de proposição, até que:

  • chegamos à cláusula vazia, {{}}\{\{\}\}, o que nos indica que a fbf inicial não é satisfazível;

  • obtemos um conjunto vazio de cláusulas, {}\{\}, que corresponde a uma tautologia, pelo que podemos admitir que a fbf inicial é satisfazível.

Chegamos sempre a um destes dois resultados, sendo esta a principal vantagem do algoritmo - chegamos sempre a um resultado concreto.

Exemplos

Δ={{P,Q},{¬P,Q},{¬Q,R},{¬R}}\Delta = \{\{P, Q\}, \{\neg P, Q\}, \{\neg Q, R\}, \{\neg R\}\}

Realizando eliminações sucessivas de PP, QQ e RR, chegamos à cláusula vazia (não confundir com conjunto vazio de cláusulas), pelo que podemos concluir que a fbf não é satisfazível:

P(Δ)={{Q},{¬Q,R},{¬R}}\exists P(\Delta) = \{\{Q\}, \{\neg Q, R\}, \{\neg R\}\}
Q(P(Δ))={{R},{¬R}}\exists Q(\exists P(\Delta)) = \{\{R\}, \{\neg R\}\}
R(Q(P(Δ)))={{}}\exists R(\exists Q(\exists P(\Delta))) = \{\{\}\}


Δ={{P,Q},{¬P,Q},{¬Q,R}}\Delta = \{\{P, Q\}, \{\neg P, Q\}, \{\neg Q, R\}\}

Realizando eliminações sucessivas de PP, QQ e RR, chegamos a um conjunto vazio de cláusulas, podendo concluir que a fbf é satisfazível:

P(Δ)={{Q},{¬Q,R}}\exists P(\Delta) = \{\{Q\}, \{\neg Q, R\}\}
Q(P(Δ))={{R}}\exists Q(\exists P(\Delta)) = \{\{R\}\}
R(Q(P(Δ)))={}\exists R(\exists Q(\exists P(\Delta))) = \{\}

Pode notar-se que na penúltima linha não são gerados resolventes-RR, mas qualquer clausula que contenha RR é removida, pelo que ficamos apenas com um conjunto vazio de cláusulas.

Uma maneira de implementar o algoritmo DP consiste em utilizar o conceito de balde, um conjunto de cláusulas. O algoritmo consiste em:

  • Criar e preencher baldes

    • Primeiro, estabelecer uma relação de ordem total entre os símbolos de proposição na fbf;

    • Criar um balde sem elementos por cada símbolo de proposição que ocorra na fbf, cada um deles designado por bPib_{P_{i}}, ordenados de acordo com a relação de ordem total previamente estabelecida;

    • Cada cláusula é colocada no primeiro balde que houver tal que a cláusula menciona PiP_{i}.

  • Processar baldes

    Para processar o balde bPib_{P_{i}}, geram-se todos os resolventes-PiP_{i} a partir exclusivamente de cláusulas do balde respetivo; cada um destes resolventes é colocado no primeiro balde seguinte bPjb_{P_{j}} tal que a cláusula mencione PjP_{j} e assim sucessivamente. Se durante o processamento de um balde for gerada a cláusula vazia, o algoritmo termina, indicando que a fbf não é satisfazível. Se chegarmos ao fim e a cláusula vazia nunca for gerada, podemos afirmar que a fbf é satisfazível.

Exemplo - Aplicação do método dos baldes

Ora, peguemos na fbf tal que

Δ={{P,Q,¬R},{¬P,S,T,R},{¬P,Q,S},{¬Q,¬R},{S}}.\Delta = \{\{P, Q, \neg R\}, \{\neg P, S, T, R\}, \{\neg P, Q, S\}, \{\neg Q, \neg R\}, \{S\}\}.

Podemos ainda estabelecer uma relação de ordem total arbitrária - seja ela:

PQRST.P \prec Q \prec R \prec S \prec T.

A primeira fase, criar e preencher os baldes, dá-se tal que:

bP:{P,Q,¬R},{¬P,S,T,R},{¬P,Q,S}bQ:{¬Q,¬R}bR:bS:{S}bT:\begin{aligned} b_{P}: & \{P, Q, \neg R\}, \{\neg P, S, T, R\}, \{\neg P, Q, S\}\\ b_{Q}: & \{\neg Q, \neg R\}\\ b_{R}: & \\ b_{S}: & \{S\}\\ b_{T}: & \\ \end{aligned}

Processar o balde bPb_{P} origina 2 novas cláusulas, nenhuma delas vazia, pelo que o algoritmo ainda não acabou (aqui uma das cláusulas está "contida" noutra, pelo que só queremos a menor):

bP:{P,Q,¬R},{¬P,S,T,R},{¬P,Q,S}bQ:{¬Q,¬R},{Q,¬R,S}bR:bS:{S}bT:\begin{aligned} b_{P}: & \{P, Q, \neg R\}, \{\neg P, S, T, R\}, \{\neg P, Q, S\}\\ b_{Q}: & \{\neg Q, \neg R\}, \qquad \qquad \qquad \qquad \qquad \qquad \{Q, \neg R, S\}\\ b_{R}: &\\ b_{S}: & \{S\}\\ b_{T}: &\\ \end{aligned}

Processar o balde bQb_{Q} origina uma nova cláusula, não vazia:

bP:{P,Q,¬R},{¬P,S,T,R},{¬P,Q,S}bQ:{¬Q,¬R},{Q,¬R,S}bR:{¬R,S}bS:{S}bT:\begin{aligned} b_{P}: & \{P, Q, \neg R\}, \{\neg P, S, T, R\}, \{\neg P, Q, S\}\\ b_{Q}: & \{\neg Q, \neg R\}, \qquad \qquad \qquad \qquad \qquad \qquad \{Q, \neg R, S\}\\ b_{R}: & \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \{\neg R, S\}\\ b_{S}: & \{S\}\\ b_{T}: & \end{aligned}

Processar os próximos baldes não gera mais nenhuma cláusula, podendo, então, afirmar que fbf é satisfazível.

Falta, contudo, um pormenor para o algoritmo DP ser considerado um algoritmo de SAT: resta devolver uma interpretação que satisfaça a fbf (isto caso seja satisfazível, claro).

Neste passo, vamos inspecionar os baldes pela ordem inversa à da relação de ordem total estabelecida inicialmente. A inspeção de um balde bPib_{P_{i}} é realizada de modo a atribuir um valor lógico ao símbolo de proposição correspondente tal que todas as suas cláusulas são satisfeitas, tendo em conta os valores lógicos já atribuídos aos outros símbolos de proposição. Pegando no exemplo anterior:

  • Começamos pelo último balde, bTb_{T}; estando o balde vazio, podemos escolher qualquer valor lógico (vamos escolher I(T)=VI(T) = V);

  • Seguimos para o balde bSb_{S}, que contém uma única cláusula, {S}\{S\}, não dependente de nenhum dos valores lógicos anteriores. Para ser satisfeita, temos de escolher I(S)=VI(S)=V;

  • Inspecionando o balde seguinte, bRb_{R}, podemos verificar que existe uma cláusula, {¬R,S}\{\neg R, S\}. Tendo S verdadeiro, ¬R\neg R poderá tomar qualquer valor, tal como RR. Podemos escolher I(R)=VI(R)=V.

  • Olhando para o balde bQb_{Q}, temos 2 cláusulas, mas procuramos sempre a que depende diretamente do valor de QQ, sendo esta {¬Q,¬R}\{\neg Q, \neg R\} neste caso; para a satisfazer, visto que RR é verdadeiro (e por consequência ¬R\neg R falso), temos de ter ¬Q\neg Q verdadeiro, e QQ, por conseguinte, falso (I(Q)=FI(Q)=F);

  • Por fim, olhando para o balde bPb_{P}, a única cláusula cuja satisfação depende de PP é {P,Q,¬R}\{P, Q, \neg R\}, onde temos necessariamente de ter PP verdadeiro - I(P)=VI(P)=V.

Uma interpretação que satisfaz Δ\Delta é, portanto, I(T)=V,I(S)=V,I(R)=V,I(Q)=F,I(P)=VI(T)=V, I(S)=V, I(R)=V, I(Q)=F, I(P)=V.

É, ainda, importante olhar para a escolha da relação de ordem total, sendo esta bastante relevante para simplificar o processo.

Se, ainda em relação à fbf anterior, tivéssemos optado pela ordem SRPQTS \prec R \prec P \prec Q \prec T, obteríamos:

bS:{¬P,S,T,R},{¬P,Q,S},{S}b_{S}: \{\neg P, S, T, R\}, \{\neg P, Q, S\}, \{S\}
bR:{P,Q,¬R},{¬Q,¬R}b_{R}: \{P, Q, \neg R\}, \{\neg Q, \neg R\}
bP:b_{P}:
bQ:b_{Q}:
bT:b_{T}:

A escolha desta ordem levou a menos processamento do que a escolha da ordem anterior, pelo que esta escolha teria sido bastante melhor (e mais simples).