Algoritmo DPLL - DPLL algorithm

DPLL

Em uma fórmula CNF-SAT : 1-Escolha um literal 2-Atribua um valor verdade a ele 3-Simplifique a fórmula 4-Verifique a satisfação; 5-Se não ficar satisfeito, volte atrás
Aula	Problema de satisfatibilidade booleana
Estrutura de dados	Árvore binária
Desempenho de pior caso	${\ displaystyle O (2 ^ {n})}$
Melhor caso de desempenho	${\ displaystyle O (1)}$ (constante)
Pior caso de complexidade de espaço	${\ displaystyle O (n)}$ (algoritmo básico)

Em lógica e ciência da computação , a Davis-Putnam-Logemann-Loveland ( DPLL ) algoritmo é uma completa , recuando baseado algoritmo de busca para decidir a satisfatibilidade de fórmulas lógica proposicional na forma normal conjuntiva , ou seja, para resolver o CNF-SAT problema.

Foi introduzido em 1961 por Martin Davis , George Logemann e Donald W. Loveland e é um refinamento do algoritmo Davis-Putnam anterior , que é um procedimento baseado em resolução desenvolvido por Davis e Hilary Putnam em 1960. Especialmente em publicações mais antigas, o O algoritmo Davis-Logemann-Loveland é frequentemente referido como o "método Davis-Putnam" ou o "algoritmo DP". Outros nomes comuns que mantêm a distinção são DLL e DPLL.

Depois de mais de 50 anos, o procedimento DPLL ainda forma a base para os solucionadores SAT completos mais eficientes. Ele foi recentemente estendido para a prova automatizada de teoremas para fragmentos de lógica de primeira ordem por meio do algoritmo DPLL (T) .

Implementações e aplicativos

O problema SAT é importante tanto do ponto de vista teórico quanto prático. Na teoria da complexidade , foi o primeiro problema que se mostrou NP-completo e pode aparecer em uma ampla variedade de aplicações, como verificação de modelo , planejamento e programação automatizados e diagnóstico em inteligência artificial .

Como tal, tem sido um tema quente na pesquisa por muitos anos, e competições entre solucionadores de SAT acontecem regularmente. Implementações modernas da DPLL como Chaff e zChaff , GRASP ou MiniSat estão nas primeiras colocações das competições nos últimos anos.

Outra aplicação que frequentemente envolve DPLL é a prova automatizada de teoremas ou teorias do módulo de satisfatibilidade (SMT), que é um problema SAT no qual variáveis ​​proposicionais são substituídas por fórmulas de outra teoria matemática .

O algoritmo

O algoritmo básico de retrocesso é executado escolhendo um literal, atribuindo um valor verdade a ele, simplificando a fórmula e, em seguida, verificando recursivamente se a fórmula simplificada é satisfatória; se for esse o caso, a fórmula original é satisfatória; caso contrário, a mesma verificação recursiva é feita assumindo o valor verdade oposto. Isso é conhecido como regra de divisão , pois divide o problema em dois subproblemas mais simples. A etapa de simplificação remove essencialmente todas as cláusulas que se tornam verdadeiras sob a atribuição da fórmula e todos os literais que se tornam falsos a partir das cláusulas restantes.

O algoritmo DPLL melhora o algoritmo de retrocesso pelo uso rápido das seguintes regras em cada etapa:

Propagação de unidade

Se uma cláusula é uma cláusula unitária , ou seja, contém apenas um único literal não atribuído, esta cláusula só pode ser satisfeita atribuindo o valor necessário para tornar este literal verdadeiro. Portanto, nenhuma escolha é necessária. A propagação de unidade consiste em remover todas as cláusulas que contêm o literal de uma cláusula de unidade e em descartar o complemento do literal de uma cláusula de unidade de cada cláusula que contém esse complemento. Na prática, isso geralmente leva a cascatas determinísticas de unidades, evitando assim uma grande parte do espaço de busca ingênuo.

Eliminação literal pura

Se uma variável proposicional ocorre com apenas uma polaridade na fórmula, ela é chamada de pura . Um literal puro sempre pode ser atribuído de uma maneira que torne verdadeiras todas as cláusulas que o contêm. Assim, quando atribuídas dessa forma, essas cláusulas não restringem mais a pesquisa, podendo ser excluídas.

A insatisfação de uma dada atribuição parcial é detectada se uma cláusula se torna vazia, ou seja, se todas as suas variáveis ​​foram atribuídas de uma forma que torna os literais correspondentes falsos. A satisfatibilidade da fórmula é detectada quando todas as variáveis ​​são atribuídas sem gerar a cláusula vazia ou, em implementações modernas, se todas as cláusulas são satisfeitas. A insatisfação da fórmula completa só pode ser detectada após pesquisa exaustiva.

O algoritmo DPLL pode ser resumido no seguinte pseudocódigo, onde Φ é a fórmula CNF :

Algorithm DPLL
    Input: A set of clauses Φ.
    Output: A Truth Value.

function DPLL(Φ)
    if Φ is a consistent set of literals then
        return true;
    if Φ contains an empty clause then
        return false;
    for every unit clause {l} in Φ do
        Φ ← unit-propagate(l, Φ);
    for every literal l that occurs pure in Φ do
        Φ ← pure-literal-assign(l, Φ);
    l ← choose-literal(Φ);
    return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {not(l)});

Nesse pseudocódigo, unit-propagate(l, Φ)e pure-literal-assign(l, Φ)são funções que retornam o resultado da aplicação da propagação da unidade e da regra literal pura, respectivamente, ao literal le à fórmula Φ. Em outras palavras, eles substituem todas as ocorrências de lpor "verdadeiro" e todas as ocorrências de not lpor "falso" na fórmula Φe simplificam a fórmula resultante. O orna returndeclaração é um operador de curto-circuito . denota o resultado simplificado de substituir "verdadeiro" por in . Φ ∧ {l}lΦ

O algoritmo termina em um dos dois casos. Ou a fórmula CNF Φé encontrada para incluir um conjunto consistente de literais - ou seja, não há le ¬lpara qualquer literal lna fórmula (há apenas literais puros). Se for esse o caso, as variáveis ​​podem ser trivialmente satisfeitas, configurando-as para a respectiva polaridade do literal abrangente na avaliação. Caso contrário, quando a fórmula contém uma cláusula vazia, a cláusula é vacuamente falsa porque uma disjunção requer pelo menos um membro que seja verdadeiro para que o conjunto geral seja verdadeiro. Nesse caso, a existência de tal cláusula implica que a fórmula (avaliada como uma conjunção de todas as cláusulas) não pode ser avaliada como verdadeira e deve ser insatisfatória.

A função DPLL em pseudocódigo somente retorna se a atribuição final satisfaz a fórmula ou não. Em uma implementação real, a atribuição de satisfação parcial normalmente também é retornada em caso de sucesso; isso pode ser derivado do conjunto consistente de literais da primeira ifinstrução da função.

O algoritmo Davis – Logemann – Loveland depende da escolha do literal de ramificação , que é o literal considerado na etapa de retrocesso. Como resultado, este não é exatamente um algoritmo, mas sim uma família de algoritmos, um para cada forma possível de escolher o literal de ramificação. A eficiência é fortemente afetada pela escolha do literal de ramificação: existem instâncias para as quais o tempo de execução é constante ou exponencial, dependendo da escolha dos literais de ramificação. Essas funções de escolha também são chamadas de funções heurísticas ou heurísticas de ramificação.

Visualização

Davis, Logemann, Loveland (1961) desenvolveram este algoritmo. Algumas propriedades deste algoritmo original são:

• Baseia-se na pesquisa.
• É a base para quase todos os solucionadores modernos de SAT.
• Ele não usa a aprendizagem ou retrocesso não-cronológica (introduzida em 1996).

Um exemplo com visualização de um algoritmo DPLL com retrocesso cronológico:

• 

  Todas as cláusulas que compõem uma fórmula CNF

• 

  Escolha uma variável

• 

  Tome uma decisão, a variável a = False (0), assim as cláusulas verdes tornam-se verdadeiras

• 

  Depois de tomar várias decisões, encontramos um gráfico de implicação que leva a um conflito.

• 

  Agora volte ao nível imediato e atribua à força o valor oposto a essa variável

• 

  Mas uma decisão forçada ainda leva a outro conflito

• 

  Volte ao nível anterior e tome uma decisão forçada

• 

  Tome uma nova decisão, mas isso leva a um conflito

• 

  Tome uma decisão forçada, mas novamente isso leva a um conflito

• 

  Voltar ao nível anterior

• 

  Continue desta forma e o gráfico de implicação final

Trabalho atual

Nos anos de 2010, o trabalho de melhoria do algoritmo foi feito em três direções:

1. Definir políticas diferentes para escolher os literais de ramificação.
2. Definir novas estruturas de dados para tornar o algoritmo mais rápido, especialmente a parte da propagação da unidade .
3. Definindo variantes do algoritmo básico de retrocesso. A última direção inclui o retrocesso não cronológico (também conhecido como salto de retorno ) e o aprendizado de cláusulas . Esses refinamentos descrevem um método de retrocesso após chegar a uma cláusula de conflito que "aprende" as causas raízes (atribuições a variáveis) do conflito para evitar chegar ao mesmo conflito novamente. Os solucionadores do SAT de Aprendizado de Cláusula Orientada a Conflitos resultantes são o que há de mais moderno em 2014

Um algoritmo mais recente de 1990 é o método de Stålmarck . Além disso, desde 1986 (ordenado reduzido), os diagramas de decisão binários também têm sido usados ​​para resolver SAT.

Relação com outras noções

Execuções de algoritmos baseados em DPLL em instâncias insatisfatórias correspondem a provas de refutação de resolução de árvore .

Veja também

• Complexidade da prova
• Herbrandização

Referências

Em geral

• Davis, Martin ; Putnam, Hilary (1960). "A Computing Procedure for Quantification Theory" . Jornal do ACM . 7 (3): 201–215. doi : 10.1145 / 321033.321034 .
• Davis, Martin; Logemann, George; Loveland, Donald (1961). "Um programa de máquina para prova de teorema" . Comunicações da ACM . 5 (7): 394–397. doi : 10.1145 / 368273.368557 . hdl : 2027 / mdp.39015095248095 .
• Ouyang, Ming (1998). "Quão boas são as regras de ramificação em DPLL?" . Matemática Aplicada Discreta . 89 (1–3): 281–286. doi : 10.1016 / S0166-218X (98) 00045-6 .
• John Harrison (2009). Manual de lógica prática e raciocínio automatizado . Cambridge University Press. pp. 79–90. ISBN 978-0-521-89957-4.

Específico

Leitura adicional

• Malay Ganai; Aarti Gupta; Dr. Aarti Gupta (2007). Soluções de verificação formal escalonáveis ​​baseadas em SAT . Springer. pp. 23–32. ISBN 978-0-387-69166-4.
• Gomes, Carla P .; Kautz, Henry; Sabharwal, Ashish; Selman, Bart (2008). "Solucionadores de satisfação". Em Van Harmelen, Frank; Lifschitz, Vladimir; Porter, Bruce (eds.). Manual de representação do conhecimento . Fundamentos da Inteligência Artificial. 3 . Elsevier. pp. 89–134. doi : 10.1016 / S1574-6526 (07) 03002-7 . ISBN 978-0-444-52211-5.