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.
ds.algorithms
reference-request
lo.logic
sat
Zirui Wang
fonte
fonte
Respostas:
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.
fonte
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.
fonte
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.
fonte
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.
fonte