Journals

• Journal on Satisfiability, Boolean Modeling and Computation

Coming Conferences and Workshops

Implementations, Benchmarks and Problem Collections

• SAT4J (Java libraries for SAT algorithms and beyond)

• UBCSAT (C library for local search algorithms)

• First International Constraint Satisfaction Solver Competition

• SIMO (C++ library for SAT)

• The SAT-Ex site (experiments, SAT algorithms, data)

• SATLIB , see also mirror (a collection of SAT solvers and problem instances)

• The Second DIMACS Challenge

• MAX-SAT instances

• CSPLib (a problem library for constraints)

• POSIT - Propositional Satisfiability Testbed (optimized version of a DPLL-like procedure by Jon W. Freeman)

• SATO (version of a DPLL-like algorithm by Hantao Zhang, with application to Quasigroup problems)

• Miroslav N. Velev (benchmarks from hardware verification)

• SAT Instance Generation Page (generators for 3-CNF's with exactly one satisfying assignment)

• Lintao Zhang's SAT Page (implementation of a DPLL-like SAT algorithm called Z-Chaff)

• BDD packages

• Forced Satisfiable CSP and SAT Benchmarks by Ke Xu

Past Conferences and Workshops

• SAT 2009 (June 30 - July 3, 2009, Swansea, UK)

• SAT 2008 (May 12 - 15 2008, Guangzhou, P. R. China)

• Ninth International Conference on Theory and Applications of Satisfiability Testing (SAT 2006) (August 12 - 15, Seattle, Washington, USA, affiliated to FLOC'06).

• SAT-2005 Eighth International Conference on Theory and Applications of Satisfiability Testing (with 2005 SAT Solver Competition and 2005 QBF Solver Evaluation June 19th-23rd 2005, University of St. Andrews Conference Centre, St. Andrews, Scotland

• SAT 2004 (May 10-13, 2004, Vancouver, Canada)

• SAT 2003 (May 5-8, 2003, S. Margherita Ligure - Portofino ( Italy)

• Dagstuhl Seminar 03141 (The Propositional Satisfiability Problems -- Algorithms and Lower Bounds; 30.03.-04.04.2003, SCHLOSS DAGSTUHL)

• TABLEAUX 2002 (as part of the Federated Logic Conference FLoC'02, July 30 - August 1, 2002 in Copenhagen, Denmark)

• SAT 2002 Cincinnati (Ohio, USA), May 6-9, 2002 (deadline for abstracts: February 6, 2002; deadline for submission of SAT solvers (and benchmarks) to the SAT solver competition: March 6, 2002)

• SAT 2001: Workshop on Theory and Applications of Satisfiability Testing June 14-15, 2001 Boston University Massachusetts; deadline March 15, 2001

• TABLEAUX 2000 July 4-7, 2000; deadline December 1, 1999

• SAT 2000, Third  Workshop on the Satisfiability Problem May 14-18, 2000; deadline April 30, 2000

• DIMACS Workshop on Faster Exact Solutions for NP-Hard Problems February 23-24, 2000; deadline December 31, 1999

• SAT'98 , May 10-14, 1998, 2nd Workshop on the Satisfiability Problem

• SAT'96 , April 29 - May 3, 1996, Siena, Italy; schedule

Homepages

• Dimitris Achlioptas (random SAT, threshold phenomena)

• Kim Allan Andersen (probabilistic SAT)

• Noriko H. Arai (resolution and Gentzen systems; reasoning with symmetries)

• Thesis of Andrew B. Baker (constraint satisfaction problems)

• Clark W. Barrett (hardware verification via SAT)

• Paul Beame (lower bounds for propositional proof systems, complexity theory)

• Richard Beigel ("3-Coloring in time O(1.3446^n): a no-MIS algorithm" and translating 3-SAT algorithms into molecular computing)

• Eli Ben-Sasson (proof complexity, especially resolution and polynomial calculus)

• Wolfgang Bibel (automated deduction)

• Armin Biere (applications of SAT, bounded model checking)

• Per Bjesse (SAT-based hardware verification (using Stalmarck's algorithm))

• Maria Paola Bonacina (automated reasoning and theorem proving)

• Maria Luisa Bonet Carbonell (propositional proof systems)

• Endre Boros (applications of operations research to SAT)

• Michael Buro (SAT competition, "On resolution with short clauses")

• Stanley N. Burris (history of mathematical logic, especially Boole's logic)

• Samuel Buss (lower bounds, bounded arithmetic)

• Philippe Chatalic (knowledge base validation)

• Stephen A. Cook (complexity theory, proof complexity)

• James M. Crawford (algorithms, random CNF's)

• Victor Dalmau (constraint satisfaction problems)

• Vijay Durairaj (applications of tree decompositions to SAT)

• Uwe Egly (random SAT and QBF)

• John Franco (probabilistic analysis of algorithms, polynomial time solvable subclasses of satisfiability)

• Alan Frisch (Artificial Intelligence, constraint satisfaction problems)

• Nicola Galesi (complexity theory, proof systems, polynomial time solvable subclasses of satisfiability)

• Zvi Galil (in the 70's important work on resolution lower bounds)

• Allen van Gelder (SAT solver, theorem proving, (propositional) resolution)

• Ian Gent (SAT by local search, empirical studies, phase transition)

• Andreas Goerdt (random SAT)

• Carla P. Gomes (randomized algorithms, heavy tails; combinatorial problems)

• Martin Grohe

• Jan Friso Groote (the propositional theorem prover HeerHugo)

• Marijn Heule (the march SAT solver family, and SAT algorithms in general)

• Edward Hirsch (upper bounds for SAT decision (sytematic and local search))

• John Hooker's Available Papers (logical inference, empirical evaluation of algorithms)

• Jinbo Huang (SAT algorithms, "Tinisat" SAT solver)

• Holger Hoos (local search algorithms, empirical analysis of algorithms)

• Russell Impagliazzo (circuit lower bounds, proof complexity)

• Gabriel Istrate (phase transition)

• Peter Jeavons (constraint satisfaction problems, dichotomy via universal algebra)

• Jan Johannsen (propositional proof systems, bounded arithmetic)

• Henry Kautz (applications of SAT algorithms to planning, local search, random SAT)

• Hans Kleine Büning (propositional logic, resolution, automated theorem proving)

• Jan Krajicek (complexity theory, logic, bounded arithmetic)

• Daniel Le Berre (implementations of SAT algorithms, SAT Live (see below), non-monotonic reasoning)

• Theodor Lettmann (calculi for automated theorem proving, complexity of logic procedures; especially a "Logic Algorithms Library")

• Reinhold Letz (automated theorem proving, proof systems)

• Hector Levesque (local search, random SAT, artificial intelligence)

• Chu Min Li (the SAT algorithm Satz)

• Mark Liffiton (symmetry detection, minimally unsatisfiable sub-formulas)

• Michael Littman (some thoughts)

• Inês Lynce (SAT algorithms, minimal unsatisfiable sub-clause-sets)

• Hans van Maaren (ellipsoid methods for SAT decision, SAT solvers, application of linear, integer and semidefinite programming to SAT)

• Johann (Janos) A. Makowsky (poly-time hierarchy for #SAT by bounded treewidth)

• Sharad Malik (hardware verification; Chaff)

• Elitza N. Maneva (belief and survey propagation, constraint satisfaction and random SAT)

• pete@ccs.neu.edu (SAT and ATP, especially ACL2)

• Victor Marek (SAT, constraint programming, SAT and van der Waerden numbers)

• Roberto Sebastiani (model checking, SMT)

• Joao Marques Silva (SAT algorithms and applications)

• Fabio Massacci (automated reasoning, DES and SAT)

• Ken McMillan (Symbolic Model Checking via OBDDs; recently also applying SAT)

• Christoph Meinel (OBDD's in VLSI design and verification; complexity theory)

• Dieter van Melkebeek (complexity theory; time/space tradeoffs for SAT)

• Jochen Messner (simplified proof of the equivalence between optimal algorithms and proof systems for SAT/UNSAT)

• Marc Mezard (statistical physics and SAT; survey propagation)

• David Mitchell (random SAT, local search, constraint satisfaction problems)

• Mike Molloy (random SAT problems)

• Remi Monasson (random SAT problems, statistical mechanics, DLL-algorithms)

• Cristopher Moore (random SAT problems, statistical physics)

• DoRon B Motter (applications of BDD to SAT solving ("compressed breadth-first search"); SAT solver Cassat)

• Rajeev Motwani (an article "Worst-case Time Bounds for Coloring and Satisfiability Problems. (with T. Feder)" is announced)

• Alexander Nadel (the SAT solver Jerusat)

• Rolf Niedermeier (fixed parameter tractability, MAXSAT)

• Robert Nieuwenhuis (SAT modulo theories)

• Albert Oliveras (SAT modulo theories)

• Ming Ouyang (SAT and integer programming)

• Christos H. Papadimitriou (complexity theory; combinatorial optimization; k-SAT bounds)

• Ramamohan Paturi (upper and lower bounds for SAT decision)

• Toniann Pitassi (lower bounds for propositional proof systems, complexity theory)

• Daniele Pretolani (hierarchies of poly-time decidable classes of CNF's, hypergraphs)

• Patrick Prosser (constraint satisfaction problems)

• Paul W. Purdom ((probabilistic) analysis of (SAT-)algorithms)

• Alexander Razborov (lower bounds for branching programs and the polynomial calculus)

• Soeren Riis (lower bounds for propositional proof systems)

• Irina Rish (DLL and the original DP algorithm (also hybrid systems); CSP)

• Andrea Roli (satisfiability by Boolean networks; parallelization of local search)

• Amitabha Roy ("robust satisfying assignments", "supermodels")

• Karem A. Sakallah (symmetries for SAT solving, minimally unsatisfiable subformulas, SAT solvers)

• Thomas Schiex (constraint satisfaction)

• John S. Schlipf (logic programming, deductive databases, complexity theory)

• Uwe Schöning (complexity theory, logic, probabilistic SAT algorithms); Section Theoretical Computer Science at University Ulm

• Bart Selman (phase transition for random k-CNF; applications of SAT to planning; local search)

• Mary Sheeran (hardware verification, Stalmarck's algorithm)

• AG Siegmann (artificial intelligence)

• Laurent Simon (the original DP-algorithm supplied with OBDD-datastructures, SAT solver Glucose)

• Carsten Sinz (visualisation of SAT instances)

• Barbara M. Smith (constraint satisfaction problems)

• William M. Spears (neural networks and simulated annealing for SAT)

• Group of Ewald Speckenmeyer

• Bruce Spencer (resolution proofs, automated reasoning)

• Stefan Szeider (SAT and graph theory)

• Michel Talagrand (probability theory of spin glasses and combinatorial problems)

• Jacobo Torán (space complexity of resolution, complexity theory)

• Klaus Truemper (logic programming, matroid theory)

• Alasdair Urquhart (lower bounds for proof systems, the resolution calculus)

• Moshe Y. Vardi (a recent paper on the hardness of random formulas for SAT solver; bounded tree-width)

• Fernandez de La Vega (random formulas)

• Gérard Verfaillie (constraint optimization problems)

• Toby Walsh (local search; translations between SAT and CSP)

• Joost P. Warners (solving satisfiability problems using elliptic approximations, branching rules, ..)

• Ingo Wegener (boolean functions, OBDD's)

• Ryan Williams (backdoors for SAT solvers; complexity theory)

• David Bruce Wilson (random problems, phase transition)

• Ke Xu (random sat, constraint satisfaction problems, phase transition)

• Francis Zane (upper bounds (deterministic and randomized) for k-SAT decision)

• Riccardo Zecchina (Statistical Physics and SAT)

• Hantao Zhang (automated reasoning, the SAT-solver SATO)

• Lintao Zhang (the SAT solver Chaff)

• Xishun Zhao (minimally unsatisfiable formulas and generalisations, quantified boolean formulas)

SAT commercial

• Greentech Computing Ltd. (UK)

• Prover Technology

Miscellaneous

• Constraint Solving and Programming (at the University of Pisa)

• Constraint Satisfaction Problems (at Oxford University)

• Computational Intelligence Research Laboratory (CIRL) of the University of Oregon

• ALGOS Group (ALGorithms for Optimization and Simulation) (Lisboa, Portugal)

• Cliques, Coloring, and Satisfiability (DIMACS series: "The Second DIMACS Challenge")

• Satisfiability Problem: Theory and Applications (DIMACS series)

• Propositional Crypto Challenges

• Photo from the SAT 2000 workshop in Renesse (click once for magnification, then click on some persons head to get connected to his/her home page)

• SAT Live (Links for the satisfiability problem)

• Automated Deduction Page (links for the field of automated deduction; maintained by Edgar Altamirano )

• Symbolic Computation Group (University Tübingen; an application of SAT in automotive product data management)

• Minimal Unsatisfiable Formulas: Structure and Algorithms (Hans Kleine Büning)

• The P versus NP Problem (Clay Institute)