Journals
Coming Conferences and Workshops
Implementations, Benchmarks and Problem Collections
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)
- 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
Miscellaneous
Oliver Kullmann
Last modified: Mon Jul 13 17:11:08 BST 2009