Algoritmos SAT não baseados em DPLL

Existem algoritmos para solução de SAT que não são baseados em DPLL? Ou todos os algoritmos usados ​​pelos solucionadores SAT são baseados em DPLL?

A Pesquisa de resolução (apenas a aplicação da regra de resolução com algumas boas heurísticas) é outra estratégia possível para os solucionadores de SAT. Teoricamente, é exponencialmente mais poderoso (ou seja, existem problemas para os quais ele tem provas mais curtas exponenciais) do que o DPLL (que apenas executa a resolução em árvore, embora você possa aumentá-lo com um bom aprendizado para aumentar seu poder - se isso o torna tão poderoso quanto a resolução geral ainda é aberto até onde sei), mas não conheço uma implementação real com melhor desempenho.

Se você não se limitar a concluir a pesquisa, o WalkSat é um solucionador de pesquisa local que pode ser usado para encontrar soluções satisfatórias e superar a pesquisa baseada em DPLL em muitos casos. Não se pode usá-lo para provar a insatisfação, a menos que alguém armazene em cache todas as atribuições que falharam, o que significaria requisitos de memória exponencial.

Editar: Esqueci de adicionar - Planos de corte também podem ser usados ​​(reduzindo o SAT para um programa inteiro). Em particular, os cortes de Gomory são suficientes para resolver qualquer programa inteiro para otimizar. Novamente, no pior caso, pode ser necessário um número exponencial. Penso que o livro Complexidade Computacional de Arora & Barak tem mais alguns exemplos de sistemas de prova que em teoria se poderia usar para algo como a solução SAT. Novamente, eu realmente não vi uma implementação rápida de nada além dos métodos baseados em DPLL ou em pesquisa local.

A propagação de pesquisa é outro algoritmo que foi usado com êxito em alguns tipos de problemas de SAT, principalmente em instâncias aleatórias de SAT. Como o WalkSAT, ele não pode ser usado para provar insatisfação, mas é baseado em idéias muito diferentes (algoritmos de passagem de mensagens) do WalkSAT.

Existem solucionadores SAT baseados na pesquisa local. Veja, por exemplo, este artigo para exposição.

Você também pode dizer que todos os solucionadores de CSP também são solucionadores de SAT. E existem até onde eu sei dois métodos usados ​​no CSP:

• DFS exaustivo com verificação do espaço de pesquisa e verificação da consistência do arco, possivelmente usando o barbear para garantir que a consistência seja mantida o mais rápido possível.
• Métodos locais (busca tabu, recozimento simulado)

O Monte Carlo Tree Search (MCTS) alcançou recentemente resultados impressionantes em jogos como o Go. A idéia básica aproximada é intercalar a simulação aleatória com a pesquisa em árvore. É leve e fácil de implementar, a página do hub de pesquisa que vinculei contém muitos exemplos, documentos e também algum código.

Previti et al. [1] fizeram algumas investigações preliminares do MCTS aplicadas ao SAT. Eles chamam o algoritmo de pesquisa baseado em MCTS UCTSAT ("limites de confiança superiores aplicados às árvores SAT", se você desejar). Eles compararam o desempenho do DPLL e UCTSAT em instâncias do repositório SATLIB, com o objetivo de verificar se o UCTSAT produziria árvores de pesquisa significativamente menores que o DPLL.

Para instâncias de coloração aleatória uniforme de 3-SAT e de gráfico plano de tamanhos diferentes, não houve diferenças significativas. No entanto, o UCTSAT teve um desempenho melhor em instâncias do mundo real. O tamanho médio das árvores (em termos de número de nós) para quatro instâncias diferentes de análise de falhas de circuito SSA foi de vários milhares para DPLL, enquanto sempre inferior a 200 para UCTSAT.

[1] Previti, Alessandro, Raghuram Ramanujan, Marco Schaerf e Bart Selman. "O UCT no estilo Monte-Carlo procura por satisfação booleana." Em AI * IA 2011: Inteligência Artificial em torno do homem e além, pp. 177-188. Springer Berlin Heidelberg, 2011.

A DPLL não especifica estritamente a ordem das visitas variáveis ​​e há muitas pesquisas interessantes que analisam as estratégias ideais de ataque de ordens variáveis. parte disso é incorporada à lógica de seleção de variáveis ​​nos algoritmos SAT. em certo sentido, algumas dessas pesquisas são preliminares, pois mostram que diferentes ordens de ataque variáveis ​​levam a diferentes restrições seqüenciais (altamente correlacionadas com a dureza da instância) e a criação de heurísticas ou estratégias mais eficazes para explorar esse insight aparentemente chave parece ser nas fases iniciais da pesquisa.

• Orientando a resolução SAT do mundo real com a decomposição dinâmica do separador de hipergrafo Li, van Beek

• Decomposição de problemas de satisfação ou Uso de gráficos para obter uma melhor compreensão dos problemas de satisfação Herwig

• The Constraintsness Knife-Edge (1998) Walsh