Material de aprendizado no SAT (problema de satisfação booleana) [fechado

Question

Quais são os bons documentos a serem lidos nos solucionadores de SAT (Problema de satisfação booleana). Não consegui encontrar um bom material via Google. Os documentos que encontrei foram os Birds Eye View, arquivos PDF muito avançados ou corrompidos ...

Quais documentos/documentos você recomenda aprender sobre os algoritmos nos solucionadores práticos de SAT modernos?

Answer 1

o Davis-Putnam-Logemann-Loveland Page na Wikipedia tem uma boa visão geral.

Então você deve ser capaz de seguir o papel Minisat "Uma solver saturada extensível".

Você também deve ler "GRASP - um novo algoritmo de pesquisa para satisfação" Para entender o algoritmo de aprendizado orientado a conflitos usado no Minisat.

Consegui escrever um solucionador de SAT em Python facilmente usando esses recursos. Meu SAT.PY O código está disponível (LGPL 2.1 atualmente), mas é bastante recente, portanto ainda pode conter bugs. Falta algumas otimizações do design Minisat; Se você quiser velocidade bruta, use o código Minisat ;-)

ATUALIZAÇÃO: Eu também fiz uma versão OCAML, SAT.ML, o que pode tornar mais fácil ver os tipos.

Answer 2

Um bom livro é: Uwe Schöning; Jacobo Torán - o problema de satisfação