Démarrage des papiers du solveur SAT

Je veux faire un premier solveur SAT. Je connais le concours SAT et la conférence SAT, et il y a tellement de papiers sur ce sujet. Je suis un démarreur, un démarreur débordé. Par où dois-je commencer? Finalement, je veux pousser l'état de l'art. Je veux des conseils d'experts sur la façon de commencer, afin de ne pas perdre trop de temps sur les éléments non essentiels. Merci beaucoup.

Un excellent aperçu pour débutant est donné par l'article suivant de 2009.

• Satisfabilité booléenne: de la dureté théorique au succès pratique , Sharad Malik, Lintao Zhang, Communications de l'ACM, 2009

Il y a plusieurs façons d'entrer dans les aspects techniques. Vous pouvez même commencer avec le papier Davis-Putnam original. Il est extrêmement clair et contient des exemples détaillés. En discutant des optimisations SAT dans un cours, nous avons découvert que quelques-uns peuvent imaginer qu'ils sont déjà là. Le document de Davis-Logeman-Loveland est (je pense) moins instructif, mais il est si court que vous pourriez aussi bien le lire.

• A Computing Procedure for Quantification Theory , Martin Davis, Hilary Putnam, Journal of the ACM, 1960.
• Un programme machine pour la démonstration de théorèmes , Martin Davis, George Logemann, Donald Loveland, Communications of the ACM, 1962.

Il y a plusieurs façons de rattraper son retard sur les développements des 50 prochaines années. Je recommanderais des diapositives de cours. La simple recherche de «DPLL» lancera de nombreux didacticiels. Si vous les parcourez, je suis sûr que la brume disparaîtra - dans une certaine mesure. Il existe également de nombreuses enquêtes utiles. Le document Zhang-Malik est un bon point de départ. Plusieurs articles du Handbook of Satisfiability peuvent vous être utiles.

• The Quest for Efficient Boolean Satisfibility Solvers , Lintao Zhang, Sharad Malik, Joint invite paper for CAV and CADE 2002.
• Handbook of Satisfiability , édité par Armin Biere, Marijn Heule, Hans van Maaren et Toby Walsh, 2009
• Anatomy and Empirical Evaluation of Modern SAT Solvers , Karem Sakallah, Joao Marques-Silva, Bulletin of the EATCS, 2011.

J'appuie la suggestion de Mikolaos. Le code MiniSAT est propre et de taille gérable. Vous pouvez jouer avec. Il existe plusieurs autres solveurs que vous pouvez essayer. CryptoMiniSat est également assez propre. Vous devriez également consulter le travail d' Armin Biere , qui écrit des solveurs SAT et écrit sur l'écriture de solveurs SAT.

Je suggère d'abord de comprendre quelles techniques ont vraiment avancé les solveurs, pour lesquelles je suggère la vue d'ensemble et l'analyse suivantes .

Ensuite, je recommanderais de télécharger le code source de minisat et de lire sa description .

Cela peut bien sûr être individuel, mais j'ai trouvé que la recherche du code source était la plus précieuse.

Si vous êtes submergé par tout le travail qui existe, pourquoi ne commencez-vous pas par prétendre que personne n'a travaillé sur le problème auparavant? Si votre objectif est de créer un solveur SAT compétitif, ce sera un voyage assez long. En commençant simplement à jouer sans «vérifier les solutions», pour ainsi dire, vous avez plus à gagner qu'à perdre.

$n$$m$$n$$m$

$n$$m$

Commencez avec un bon papier d'enquête. Il est facile d'attaquer le sujet au coup par coup et d'être confondu par différents noms dans la littérature pour les mêmes techniques et le même nom utilisé pour différentes techniques. Il est également facile de reconstituer d'anciennes batailles algorithmiques (listes d'occurrences vs listes tête-biche contre deux littéraux surveillés pour les implémentations DPLL par exemple) si vous ne savez pas quel est l'état de l'art.

Solveurs de satisfaction par Gomes, et. Al. vous donnera la configuration approximative de la terre.

Améliorer les solveurs SAT en utilisant des techniques de pointe de Manthey vous rapprochera du présent.