Einleitung und Grundlagen

• Jun Gu, Paul W. Purdom, John Franco und Benjamin W. Wah, "Algorithms for the Satisfiability (SAT) Problem: A Survey." In: Ding-Zhu Du, Jun Gu, und Panos Pardalos (Hrsg.), "Satisfiability Problem: Theory and Applications." DIMACS Series in Discrete Mathematics and Theoretical Computer Science, S. 19–152, AMS, 1997

Die Originaldarstellung des DPLL-Kalküls für Logik erster Stufe von Davis et al.:

• Martin Davis und Hilary Putnam, "A Computing Procedure for Quantification Theory." Journal of the ACM, 7(3):201–215, 1960
• Martin Davis, George Logemann und Donald Loveland, "A Machine Program for Theorem-Proving." Communications of the ACM, 5(7):394–397, 1962

Implementierung von SAT-Solvern

Die wichtigsten Techniken für DPLL-basierte SAT-Solver:

• David G. Mitchell, "A SAT Solver Primer." EATCS Bulletin (The Logic in Computer Science Column), 85:112–133, 2005
• Ilya Shlyakhter, "Main Techniques for Solving Real-World SAT Instances."

Der SAT-Solver GRASP:

• João P. Marques Silva und Karem A. Sakallah, "GRASP: A Search Algorithm for Propositional Satisfiability." IEEE Transactions on Computers, 48(5):506–521, 1999

Die SAT-Solver Chaff und zChaff:

• Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang und Sharad Malik, "Chaff: Engineering an Efficient SAT Solver." 38th ACM/IEEE Design Automation Conference, S. 530–535, 2001
• Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz und Sharad Malik, "Efficient Conflict Driven Learning in a Boolean Satisfiability Solver." 2001 IEEE/ACM International Conference on Computer Aided Design, S. 279–285, 2001
• Lintao Zhang, "Searching for Truth: Techniques for Satisfiability of Boolean Formulas." Doktorarbeit, Princeton University, Department of Electrical Engineering, 2003

Detaillierte Darstellung des MiniSat-Beweisers:

• Niklas Een und Niklas Sörensson, "An Extensible SAT-solver (extended version 1.2)." 6th International Conference on Theory and Applications of Satisfiability Testing, LNCS 2919, S. 502–518, Springer, 2003

Berechnung kleiner bzw. minimaler unerfüllbarer Kerne für unerfüllbare Formeln:

• Lintao Zhang und Sharad Malik, "Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formula." 6th International Conference on Theory and Applications of Satisfiability Testing, 2003
• Ines Lynce and João Marques-Silva, "On Computing Minimum Unsatisfiable Cores." 7th International Conference on Theory and Applications of Satisfiability Testing, 2004

SAT und Theorieschließen

Nelson-Oppen-Verfahren und Shostak-Verfahren:

• Zohar Manna und Calogero G. Zarba, "Combining Decision Procedures." Formal Methods at the Crossroads: From Panacea to Foundational Support, LNCS 2757, Springer, 2003
• David Cyrluk, Patrick Lincoln und Natarajan Shankar, On Shostak's Decision Procedure for Combinations of Theories." 13th International Conference on Automated Deduction, LNCS 1104, S. 463–477, Springer, 1996
• Cesare Tinelli und Mehdi Harandi, "A New Correctness Proof of the Nelson-Oppen Combination Procedure." F. Baader and K. U. Schulz (Hrsg.), "Frontiers of Combining Systems: 1st International Workshop", S. 103–120, Kluwer, 1996

DPLL(T)-Verfahren:

• Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras und Cesare Tinelli, "DPLL( T): Fast Decision Procedures." International Conference on Computer-Aided Verification, LNCS 3114, S. 175–188, Springer, 2004
• Robert Nieuwenhuis, Albert Oliveras, und Cesare Tinelli, "Abstract DPLL and Abstract DPLL Modulo Theories." 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LNCS 3452, S. 36–50, Springer, 2005

Verzögerte Theoriekombination:

• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Silvio Ranise, Peter van Rossum und Roberto Sebastiani, "Efficient Theory Combination via Boolean Search." Information and Computation, 204(10):1493–1525, 2006
• Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio und Roberto Sebastiani, "Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis." Technischer Bericht DIT-06-032, Informatica e Telecomunicazioni, University of Trento, 2006

Die Originalartikel von Nelson, Oppen und Shostak. Eher von historischem Interesse:

• Greg Nelson und Derek C. Oppen, "A Simplifier Based on Efficient Decision Algorithms." 5th ACM Symposium on Principles of Programming Languages, S. 141–150, 1978
• Greg Nelson und Derek C. Oppen, "Simplification by Cooperating Decision Procedures." ACM Transactions on Programming Languages and Systems, 1(2):245–257, 1979
• Greg Nelson und Derek C. Oppen, "Fast Decision Procedures Based on Congruence Closure." Journal of the ACM, 27(2):356–364, 1980
• Robert E. Shostak, "An Algorithm for Reasoning About Equality." Communications of the ACM, 21(7):583–585, 1978
• Robert E. Shostak, "Deciding Combinations of Theories." Journal of the ACM, 31(1):1–12, 1984

Anwendungen von SAT

Übersicht über Anwendung von SAT-basierten Methoden im Bereich formaler Verifikation:

• Mukul R. Prasad, Armin Biere und Aarti Gupta, "A Survey of Recent Advances in SAT-Based Formal Verification." International Journal on Software Tools for Technology Transfer, 7(2):156–173, 2005

Systembeschreibungen:

• David L. Detlefs, K. Rustan M. Leino, Greg Nelson und James B. Saxe, "Extended Static Checking." Technischer Bericht SRC-RR-159, HP Labs, 1998
• David Detlefs, Greg Nelson und James B. Saxe, "Simplify: A Theorem Prover for Program Checking." Technischer Bericht HPL-2003-148, HP Labs, 2003
• Thomas Ball, Shuvendu K. Lahiri und Madanlal Musuvathi, "Zap: Automated Theorem Proving for Software Analysis." 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LNCS 3835, S. 2–22, Springer, 2005

Lokalsuchalgorithmen

Die SAT-Solver GSAT und GWSAT:

• Bart Selman und Henry Kautz, "Local Search Strategies for Satisfiability Testing." Michael Trick und David Stifler Johnson (Hrsg.), "2nd DIMACS Challange on Cliques, Coloring, and Satisfiability", 1996

Vollständige lokale Suche:

• Hai Fang und Wheeler Ruml, "Complete Local Search for Propositional Satisfiability." 19th National Conference on Artificial Intelligence, 2004

Experimenteller Vergleich verschiedener Lokalsuchstrategien:

• Holger H. Hoos and Thomas Stützle, "Local Search Algorithms for SAT: An Empirical Evaluation." Journal of Automated Reasoning, 24(4):421–481, 2004

Ein probabilistischer O((2 (k - 1) / k)^n)-Algorithmus für k-SAT:

• Uwe Schöning, "A Probabilistic Algorithm for k -SAT Based on Limited Local Search and Restart." Algorithmica, 32(4), 2002

Ein deterministischer O((2 - 2 / (k + 1))^n)-Algorithmus für k-SAT:

• Evgeny Dantsina, Andreas Goerdt, Edward A. Hirsch, Ravi Kannand, Jon Kleinberg, Christos Papadimitriou, Prabhakar Raghavang, Uwe Schöning, "A deterministic (2 - 2 / (k + 1))^n algorithm for k-SAT based on local search." Theoretical Computer Science, 289:69–83, 2002

Random k-SAT

Backbone-Heuristik:

• Olivier Dubois und Gilles Dequen, "A Backbone Search Heuristic for Efficient Solving of Hard 3-SAT Formulae." 17th International Joint Conference on Artificial Intelligence, S. 248–253, 2001
• Gilles Dequen und Olivier Dubois, "kcnfs: An Efficient Solver for Random k-SAT Formulae." 7th International Conference on Theory and Applications of Satisfiability Testing, LNCS 2919, S. 486–501, Springer, 2004
• Gilles Dequen und Olivier Dubois, "An Efficient Approach to Solving Random k-SAT Problems." Journal of Automated Reasoning, 37(4):261–276, 2006

Weitere Literatur zu Random k-SAT gibt es in Papierform...

Strukturelle Methoden

Geordnete binäre Entscheidungsbäume:

• Randal E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation." IEEE Transactions on Computers, C-35-8:677–691, 1986
• Randal E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams." ACM Computing Surveys, 24(3):293–318, 1992
• Tomas E. Uribe und Mark E. Stickel, "Ordered Binary Decision Diagrams and the Davis-Putnam Procedure." 1st International Conference on Constraints in Computational Logics, LNCS 845, S. 34–49, Springer, 1994

Quantifizierte Boolesche Formeln

Der QBF-Solver Quaffle:

• Lintao Zhang und Sharad Malik, "Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation." Principles and Practice of Constraint Programming: 8th International Conference, LNCS 2470, S. 200, Springer, 2004
• Lintao Zhang, "Searching for Truth: Techniques for Satisfiability of Boolean Formulas." Doktorarbeit, Princeton University, Department of Electrical Engineering, 2003

QBF-spezifische Probleme:

• Carlos Ansotegui, Carla P. Gomes und Bart Selman, "The Achilles’ Heel of QBF.", 20th National Conference on Artificial Intelligence, 2005
• Ashish Sabharwal, Carlos Ansotegui, Carla P. Gomes, Justin W. Hart und Bart Selman, "QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency." 9th International Conference on Theory and Applications of Satisfiability Testing, LNCS 4121, S. 382–395, Springer, 2006

Der QBF-Solver IQTest:

• Lintao Zhang, "Solving QBF with Combined Conjunctive and Disjunctive Normal Form." 21st National Conference on Artificial Intelligence, 2006

SAT-Algorithmen für Nichtklausel-Formeln

Nichtklausel-DPLL:

• Christian Thiffault, Fahiem Bacchus und Toby Walsh, "Solving Non-clausal Formulas with DPLL Search." Principles and Practice of Constraint Programming, LNCS 3258, S. 663–678, Springer, 2005

General Matings:

• Himanshu Jain, Constantinos Bartzis und Edmund Clarke, "Satisfiability Checking of Non-clausal Formulas using General Matings." 9th International Conference on Theory and Applications of Satisfiability Testing, 2006

Tableaux:

• Tommi A. Junttila und Ilkka Niemelä, "Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking." Computational Logic: 1st International Conference, LNCS 1861, S. 553, Springer, 2004