O algoritmo de Davis‑Putnam (DPLL)

Uma fórmula da lógica proposicional é satisfazível se existe pelo menos uma valoração das suas variáveis que a torna verdadeira (V). Se é falsa em todas as valorações, é insatisfazível.

Saber se uma fórmula é satisfazível é um problema central em Ciência de Computadores, porque muitos problemas de outras áreas se podem escrever nesses termos: otimização (planeamento, horários), combinatória (coloração de grafos) e teorias de primeira ordem (os solvers SMT). Os programas que o resolvem chamam-se SAT solvers.

A forma mais direta de responder é construir a tabela de verdade e procurar uma linha em que a fórmula dê V. Com n variáveis a tabela tem 2ⁿ linhas: cada variável a mais duplica o trabalho. E, no pior caso, não se conhece nada melhor: não se conhece nenhum algoritmo para SAT que não seja exponencial no número de variáveis e de conectivos da fórmula (SAT é NP-completo).

Mas, no caso geral, dá para fazer bem melhor do que a força bruta. A ideia é construir aos poucos uma valoração parcial que satisfaça a fórmula, em vez de gerar valorações completas (linhas da tabela) e verificar cada uma. É isto que o algoritmo de Davis-Putnam faz, e fica especialmente simples com a fórmula em forma normal conjuntiva (FNC), escrita como um conjunto de cláusulas: o tema da §2.

Um literal é uma variável (p) ou a negação de uma variável (¬p). Uma cláusula é uma disjunção de literais l₁ ∨ l₂ ∨ … ∨ lₙ, com n ≥ 0, e pode ser representada pelo conjunto dos seus literais: p ∨ ¬q ∨ ¬p ∨ s é representada por {p, ¬q, ¬p, s}. Como é um conjunto, a ordem não importa e um literal repetido conta só uma vez.

Se n = 0, a cláusula é vazia e corresponde a F: não tem nenhum literal que a possa tornar verdadeira. Se n = 1, a cláusula é unitária (por exemplo, {¬p}).

Qualquer fórmula em FNC pode ser representada por um conjunto de cláusulas, lido como a conjunção dessas cláusulas. Por exemplo, ¬p ∧ (q ∨ r ∨ q) ∧ (¬r ∨ ¬s) ∧ (p ∨ s) ∧ (¬q ∨ ¬s) corresponde ao conjunto {{¬p}, {q, r}, {¬r, ¬s}, {p, s}, {¬q, ¬s}}. Também é comum escrever cada cláusula como disjunção: {¬p, q ∨ r, ¬r ∨ ¬s, …}.

Daqui saem os dois casos em que o algoritmo termina. O conjunto vazio {} não tem nenhuma cláusula para satisfazer, por isso é satisfazível. Um conjunto que contém F tem uma cláusula que nenhuma valoração torna verdadeira, por isso é insatisfazível.

Na ferramenta podes escrever um conjunto em qualquer das três notações: a compacta das linhas «Entrada» dos exercícios (p1, -p1 -p2), a de conjuntos ou a lógica. Experimenta no conversor: o mesmo conjunto aparece nas três.

Literais complementares: dado um literal l, o complementar l̃ é ¬l se l é uma variável (literal positivo) e é p se l é da forma ¬p (literal negativo). Por exemplo, o complementar de p é ¬p e o complementar de ¬p é p.

Uma cláusula é uma tautologia se contém um par de literais complementares p e ¬p, como {p, ¬q, ¬p, s}. É verdadeira em qualquer valoração, por isso pode ser retirada do conjunto sem alterar a satisfazibilidade. Aqui as tautologias são assinaladas mas não retiradas: o DLL da ferramenta trata-as como as outras cláusulas.

Uma cláusula unitária {l} tem um só literal, por isso só é verdadeira se l for verdadeiro. Aqui não há nada a escolher: qualquer valoração que satisfaça S tem de tornar l verdadeiro. A propagação unitária aproveita isto para simplificar S sem perder nenhuma solução.

Dado um conjunto de cláusulas S, obtém-se S′ por propagação unitária repetindo a transformação seguinte: se S contém uma cláusula unitária l, então

1. removem-se de S todas as cláusulas da forma l ∨ C′ (ficam verdadeiras quando l é verdadeiro; a própria {l} também sai);
2. substitui-se em S cada cláusula da forma l̃ ∨ C′ pela cláusula C′ (l̃ é falso, por isso já não ajuda a satisfazer a cláusula).

No diagrama propaga-se p: {p} e p ∨ q contêm p e saem (regra 1); ¬p ∨ r perde ¬p e fica r (regra 2); q ∨ s não tem p nem ¬p e fica igual.

Repara que a regra 2 pode criar cláusulas unitárias novas (¬p ∨ r ficou r), por isso repete-se a transformação enquanto houver unitárias. E se a cláusula {l̃} também estiver em S, perde o seu único literal e fica F, a cláusula vazia: o conjunto é insatisfazível.

Experimenta com o conjunto abaixo: clica numa cláusula unitária para a propagar e vê as duas regras a funcionar. Neste exemplo chega-se a F só com propagação unitária.

No pseudocódigo do DLL este passo é S := propagate(S). A ferramenta propaga um literal de cada vez e usa sempre a primeira cláusula unitária pela ordem do conjunto; aqui podes escolher outra para veres que as regras são as mesmas. Quando a propagação para sem S vazio e sem F, é preciso escolher um literal e ramificar: é o tema da §4.

Quando a propagação unitária para, S está num de três casos: está vazio (todas as cláusulas ficaram satisfeitas, logo S é satisfazível), contém F (há uma cláusula que nenhuma valoração satisfaz, logo S é insatisfazível) ou nenhum dos dois. No terceiro caso não há mais nada a deduzir e é preciso experimentar: escolhe-se um literal l e tenta-se primeiro S ∪ {l}; se esse ramo for insatisfazível, tenta-se S ∪ {l̃}. É o algoritmo DLL (Davis, Logemann e Loveland), em pseudocódigo:

Acrescentar {l} a S é acrescentar uma cláusula unitária, por isso a chamada recursiva DLL(S ∪ {l}) começa logo por propagar l. Como qualquer valoração torna l ou l̃ verdadeiro, S é satisfazível se e só se S ∪ {l} ou S ∪ {l̃} o for: os dois ramos cobrem todos os casos, e o algoritmo só responde insatisfazível quando todos os ramos chegam a F.

O mesmo algoritmo em fluxograma, com um exemplo de dois ramos, {¬p ∨ ¬q, ¬p ∨ q, p ∨ ¬q, p ∨ q}. Este conjunto não tem cláusulas unitárias, por isso é preciso escolher um literal logo à partida. Avança passo a passo e vê que caixa do fluxograma corresponde a cada passo; as setas a tracejado são as chamadas recursivas, que voltam ao início com o conjunto novo.

A ferramenta escolhe sempre a primeira variável por ordem alfabética com o ramo positivo primeiro, por isso aqui começa por p; começar por ¬p também seria válido. Neste exemplo não faz diferença: nos dois ramos a propagação dá {¬q, q} e depois {F}, e DLL(S) devolve insatisfazível. Na §5 vês quando a escolha do literal muda o tamanho da árvore.

Quando a propagação para e S não está vazio nem contém F, o DLL tem de escolher um literal: é o l := select_literal(S) do pseudocódigo. Esta função pode ser vista como um parâmetro do algoritmo, porque uma escolha adequada do literal pode torná-lo mais eficiente. A resposta (satisfazível ou insatisfazível) é sempre a mesma; o que muda é o caminho e o tamanho da árvore. Critérios possíveis são escolher uma variável que:

• ocorre mais vezes;
• tem o produto das ocorrências de l e de l̃ máximo;
• ocorre mais vezes nas cláusulas de tamanho mínimo;
• etc.

Escolhida a variável, falta o sinal, ou seja, qual dos dois ramos se tenta primeiro. Pode começar-se por p ou por ¬p; a ferramenta usa sempre a primeira variável por ordem alfabética e o ramo positivo primeiro. Num conjunto insatisfazível o sinal não muda o tamanho da árvore: o DLL só responde insatisfazível depois de os dois ramos chegarem a F, por isso muda só a ordem. Num conjunto satisfazível, acertar no ramo à primeira poupa o outro ramo inteiro.

Compara as duas escolhas no mesmo conjunto. Cada nó é uma chamada DLL(S); as folhas acabam em ✓ (S vazio) ou ✗ (S contém F). Experimenta também os critérios acima: no conjunto de 8 variáveis, com o ramo positivo primeiro, a ordem alfabética dá 6 nós e a variável que ocorre mais vezes nas cláusulas de tamanho mínimo dá 3.

Nenhum sinal é sempre o melhor: em «Três variáveis B» ganha o ramo positivo e em «Três variáveis E» ganha o ramo ¬. É por isso que os critérios acima olham para o conjunto em vez de seguirem uma ordem fixa. A ferramenta fica com a ordem alfabética e p primeiro, uma regra fixa e fácil de seguir à mão, para que possas comparar a tua resolução com o Passo a passo. Se escolheres outro literal o caminho muda, mas a conclusão é a mesma.

O algoritmo de Davis-Putnam, de 1960, é uma versão inicial que ainda é a base de muitos dos algoritmos mais eficientes de hoje (como os da SAT Competition). A ideia básica é considerar os valores de verdade possíveis de cada variável e simplificar a fórmula de acordo com eles até se poder concluir se é satisfazível ou não.

Essa versão de 1960, de Martin Davis e Hilary Putnam (artigo «A Computing Procedure for Quantification Theory», no Journal of the ACM), trabalhava com um conjunto de cláusulas e três regras: a propagação de cláusulas unitárias (a da §3), a eliminação de literais puros (se o complementar de l não aparece em S, pode tornar-se l verdadeiro e as cláusulas com l saem) e a eliminação de uma variável por resolução. Não havia ramificação: o conjunto ia sendo transformado até ficar vazio (satisfazível) ou conter F (insatisfazível).

A resolução junta duas cláusulas com literais complementares: de p ∨ C e ¬p ∨ D tira-se o resolvente C ∨ D. Qualquer valoração que satisfaça as duas satisfaz C ∨ D, porque p ou ¬p é falso. Para eliminar p, substituem-se todas as cláusulas com p e com ¬p por todos os resolventes desses pares; o conjunto novo já não tem p e é satisfazível se e só se S o for. Os resolventes que são tautologias podem ser descartados. Na figura, o exemplo com dois ramos da §4: eliminar p dá {¬q, q} (dois dos quatro resolventes são tautologias) e a propagação de ¬q deixa F.

O problema é o tamanho. Se p aparece em k cláusulas e ¬p em m, a eliminação troca essas k + m cláusulas por até k · m resolventes, e cada um pode ser mais comprido do que as cláusulas de onde veio. Em muitos conjuntos o número de cláusulas explode e, nos computadores da época, a memória não chegava.

Em 1962, Martin Davis, George Logemann e Donald Loveland («A Machine Program for Theorem-Proving», na Communications of the ACM) trocaram a eliminação por resolução pela ramificação: escolher um literal l e tentar S ∪ {l} e depois S ∪ {l̃}, como na §4. Em vez de guardar um conjunto cada vez maior, explora-se uma árvore em profundidade e só se guarda o caminho atual. É este algoritmo, o DLL (também chamado DPLL), que muitas vezes também se apresenta com o nome de Davis-Putnam e que esta ferramenta usa.

Oito perguntas para confirmares o que leste: umas de escolha múltipla e outras de «qual o próximo passo?», em que fazes de DLL. Depois de cada resposta vês o porquê, com a regra que se aplica. O teu melhor resultado fica guardado neste navegador.