Iniciando os papéis do SAT Solver

24

Eu quero fazer um primeiro solucionador de SAT. Conheço a competição do SAT e a conferência do SAT, e há tantos artigos sobre esse assunto. Eu sou um iniciante, um iniciante oprimido. Por onde devo começar? Eventualmente, eu quero empurrar o estado da arte. Quero alguns conselhos de especialistas sobre como começar, para não desperdiçar meu tempo com os não essenciais muito cedo. Muito Obrigado.

Zirui Wang
fonte
6
Você já implementou o algoritmo DPLL? Você ajustou e poliu sua implementação para que ela seja executada com extrema rapidez?
Jukka Suomela
5
Manual de satisfação - amazon.co.uk/… (talvez verifique uma biblioteca, o custo é bastante alto).
MGwynne
11
@Jukka: comentário -> resposta?
Suresh Venkat
4
Eu discordo de Jukka. Por que reinventar a roda? Não há motivo para refazer o que o MiniSAT já fornece código aberto. Se você estiver interessado em adicionar à estrutura CDCL, sua adição será exibida com desempenho aprimorado do MiniSAT. Além disso, a DPLL por si só não é suficiente; muitas melhorias foram feitas. Basicamente, siga a resposta do Mikolas!
Huck Bennett
11
Veja também a pergunta relacionada cstheory.stackexchange.com/q/1988
András Salamon

Respostas:

18

Uma excelente visão geral para iniciantes é fornecida pelo artigo a seguir de 2009.

Existem várias maneiras de entrar nos aspectos técnicos. Você pode até começar com o artigo original de Davis-Putnam. É extremamente claro e tem exemplos detalhados. Ao discutir as otimizações de SAT em um curso, descobrimos que alguns podem imaginar que já estão lá. O artigo de Davis-Logeman-Loveland é (me sinto) menos instrutivo, mas é tão curto que você pode lê-lo.

Existem várias maneiras de acompanhar os desenvolvimentos dos próximos 50 anos. Eu recomendaria slides para palestras. Apenas procurar por 'DPLL' exibirá muitos tutoriais. Se você navegar por eles, tenho certeza que a névoa vai clarear - até certo ponto. Existem também muitas pesquisas úteis. O artigo de Zhang-Malik é um bom ponto de partida. Existem vários artigos no Manual de Satisfação que você pode achar úteis.

Eu segundo a sugestão de Mikolaos. O código MiniSAT é limpo e de tamanho gerenciável. Você pode brincar com isso. Existem vários outros solucionadores que você pode tentar. O CryptoMiniSat também é bastante limpo. Você também deve consultar o trabalho de Armin Biere , que escreve sobre solucionadores de SAT e escreve sobre como escrever sobre solucionadores de SAT.

Vijay D
fonte
17

Sugiro primeiro entender quais técnicas realmente avançaram nos solucionadores, para as quais sugiro a seguinte visão geral e análise .

Então eu recomendaria baixar o código fonte do minisat e ler sua descrição .

É claro que pode ser individual, mas achei o código mais valioso.

Mikolas
fonte
9

Se você está impressionado com todo o trabalho disponível, por que não começa a fingir que ninguém havia trabalhado no problema antes? Se seu objetivo for criar um solucionador SAT competitivo, será uma jornada bastante longa. Ao começar a brincar sem "verificar as soluções", por assim dizer, você tem mais a ganhar do que a perder.

nmnm

nm

James King
fonte
9

Comece com um bom trabalho de pesquisa. É fácil atacar o assunto aos poucos e ficar confuso com nomes diferentes na literatura para as mesmas técnicas e o mesmo nome usado para diferentes técnicas. Também é fácil reencenar batalhas algorítmicas antigas (listas de ocorrências vs. listas iniciais vs. dois literais assistidos para implementações de DPLL, por exemplo) se você não sabe qual é o estado da arte.

Solvers de satisfação por Gomes, et. al. lhe dará a configuração áspera da terra.

Melhorando os solventes SAT Usando técnicas de última geração da Manthey, você se aproximará do presente.

Kyle Jones
fonte