Updated 3 May 2002

SAT 2002

Fifth  International Symposium on the
Theory and Applications of Satisfiability Testing

May 6-9, 2002
Cincinnati, Ohio, USA


Sunday, 5 May

08:00 - 10:00 Reception, Conference Center
Hors d'oeuveres, bar. One complementary drink.

Monday, 6 May

08:45 - 09:00 Opening Address and Welcome
09:00 - 09:45 Uwe Schöning, Universität Ulm, Germany (Keynote Talk)
New worst case bounds on k-SAT     Presentation
09:45 - 10:10 Nadia Creignou, Université de la Méditeraneé, Marseille, France (with Hervé Daudé)
Random generalized satisfiability problems
10:10 - 10:35 Akihiro Matsuura, Kyoto University, Japan (with Kazuo Iwama)
Inclusion-exclusion for k-CNF formulas
10:35 - 10:50    Coffee Break
10:50 - 11:15 John Slaney, Australian National University, Australia (with Toby Walsh)
Phase Transition Behavior: From Decision to Optimization
11:15 - 11:40 Alexis C. Kaporis, University of Patras, Greece (with Lefteris M. Kirousis and Efthimios G. Lalas))
The Probabilistic Analysis of a Greedy Satisfiability Algorithm
11:40 - 12:05 Alan Frieze, Carnegie Mellon University, USA (with Nicolas Wormald)
k-SAT: A tight threshold for moderately growing k
12:05 - 01:30 Lunch
01:30 - 01:55 Stefan Szeider, Austrian Academy of Sciences, Austria
Generalizations of matched CNF formulas
01:55 - 02:20 Oliver Kullmann, University of Wales, Swansea, United Kingdom
Towards an adaptive density based branching rule for SAT solvers, using a database for mixed
random conjunctive normal forms built upon the Advanced Encryption Standard (AES)
02:20 - 02:45 Hans Kleine Büning, Universität Paderborn, Germany (with Daoyun Xu)
The complexity of homomorphisms and renamings of minimal unsatisfiable formulas
02:45 - 03:10 Stefan Porschen, Universität zu Köln, Germany (with Bert Randerath and Ewald Speckenmeyer)
X3SAT is decidable in time O(2n/5)
03:10 - 03:30 Coffee Break
03:30 - 03:55 Remi Monasson, CNRS-Laboratoire de Physique Théorique de l'ENS, France (with Simona Cocco)
Restart method and exponential acceleration of random 3-SAT instances resolutions:
A large deviation analysis of the Davis-Putnam-Loveland-Logemann algorithm
03:55 - 04:20 Eugene Goldberg, Cadence Berkeley Labs, USA
Testing satisfiability of CNF formulas by computing a stable set of points
04:20 - 04:45 Franc Brglez, North Carolina State University, USA (with Xiao Yu Li and Matthias F. Stallmann)
The role of a skeptic agent in testing and benchmarking of SAT algorithms
04:45 - 05:00 Short Coffee Break
SAT Solver Presentations
05:00 - 05:54 Short presentations by groups who do not have regular papers in the program
05:00 - 05:06 Oliver Kullmann    OKsolver
05:06 - 05:12 Allen Van Gelder    MODOC
05:12 - 05:18 Allen Van Gelder    Rb2Cl
05:18 - 05:24 John Kolen    Partsat
05:24 - 05:30 Daniel Le Berre for Richard Ostrowski    LSAT (with Bertrand Mazure, Lakhdar Sais)
05:30 - 05:36 Marijn Heule    March (with Hans van Maaren, Mark Dufour, Joris van Zwieten)
05:36 - 05:42 Eugene Goldberg    Berkmin (with Yakov Novikov)
05:42 - 05:48 Armando Tacchella    Simo (with Enrico Giunchiglia, Massimo Maratea)
05:48 - 05:54 João Marques-Silva    Jquest (with Inês Lynce)
06:10 - 00:00 Dinner, Conference Center

Tuesday, 7 May

08:05 - 08:50 João Marques-Silva, Universidade Técnica de Lisboa, Portugal (Keynote Talk)
Hypothetical reasoning in propositional satisfiability
08:50 - 09:15 Olivier Dubois, Université Paris 6, France (with Gilles Dequen)
Renormalization as a function of clause lengths for solving random k-SAT formulae
09:15 - 09:40 Allen Van Gelder, University of California at Santa Cruz, USA
Toward leaner binary-clause reasoning in a satisfiability solver
09:40 - 10:05 Harald Ruess, SRI International, USA (with Leonardo de Moura)
Lemmas on demand for Satisfiability solvers
10:05 - 10:25    Coffee Break
10:25 - 10:50 Chu Min Li, University of Picardie Jules Verne, France (with Bernard Jurkowiak and Paul Walton Purdom)
Integrating symmetry breaking into a DLL procedure
10:50 - 11:15 Ian Gent, University of St. Andrews, Scotland (with Patrick Prosser)
SAT encodings of the stable marriage problem with ties and incomplete lists
11:15 - 11:40 Inês Lynce, Technical University of Lisbon, Portugal (with João Marques-Silva)
Efficient data structures for backtrack search SAT solvers
11:40 - 12:05 Zbigniew Stachniak, York University, Canada
Going non-clausal
12:05 - 01:30 Lunch
01:30 - 01:55 Renato Bruni, Università di Roma "La Sapienza", Italy
Exact selection of minimal unsatisfiable subformulae for special classes of propositional formulae
01:55 - 02:20 Fadi A. Aloul, University of Michigan, USA (with Arathi Ramani, Igor Markov, and Karem Sakallah)
Solving difficult SAT instances in the presence of symmetry
02:20 - 02:45 Andrea Roli, Università degli Studi di Bologna, Italy
Impact of structure on parallel local search for SAT
02:45 - 03:10 Dimitris Achlioptas, Microsoft Research, USA (with Chris Moore)
A bit of abstinence (provably) promotes satisfaction
03:10 - 03:30 Coffee Break
Quantified Boolean Formulas Mini Workshop I
03:30 - 03:55 J. Dan Pehoushek, USA
Introduction to Q space
03:55 - 04:20 Andrew G.D. Rowley, St. Andrews University, Scotland (with Ian Gent)
Solving 2-CNF quantified boolean formulae using variable assignment and propagation
04:20 - 04:45 Anja Remshagen, State University of West Georgia, USA (with Klaus Truemper)
Algorithms for logic-based abduction
04:45 - 05:10 Subramanyan Siva, University of Cincinnati, USA (with W. Mark Vanfleet, John Schlipf, Ranga Vemuri, and John Franco)
Reconfigurable interconnect synthesis via quantified Boolean satisfiability
QBF and SAT Solver Business Meetings
05:10 - 06:00 Where to have the next QBF meeting and SAT solver competition, etc.
06:00 - 10:00 Excursion and Dinner
An old fashioned American recreational experience: a picnic at Cincinnati's Cinergy
Field while watching a classic baseball game pitting the Cincinnati Reds, America's
oldest professional baseball team, against the Milwaukee Brewers. We will watch the
proceedings from the middle deck in a private glass-enclosed room. The following
will be served continuously, buffet style, for our enjoyment: Hot Dogs, Fried Chicken,
Crudites, Fruit, Cheese, Potato Salad, String Beans, Soft Drinks, and Draft Beer. Have
as much as you want. Baseball/Cricket expert Ian Gent will be on hand to explain
what you see (Gent denies he is an expert but we will see once the battle is engaged).

Wednesday, 8 May

08:05 - 08:50 Edmund Clarke, Carnegie Mellon University, USA (Keynote Talk)
SAT based abstraction refinement in temporal logic model checking
08:50 - 09:15 Oded Maler, Verimag, France (with Moez Mahfoudh, Peter Niebert, and Eugene Asarin)
A satisfiability checker for difference logic
09:15 - 09:40 Fadi A. Aloul, University of Michigan, USA (with Brian Sierawski and Karem Sakallah)
A tool for measuring progress of backtrack-search solvers
09:40 - 10.05 Inês Lynce, Technical University of Lisbon, Portugal (with João Marques-Silva)
Complete unrestricted backtracking algorithms for satisfiability
10:05 - 10:25    Coffee Break
10:25 - 10:50    Daniele Pretolani, Università di Camerino, Italy
Probabilistic logic: The PSAT and CPA models
10:50 - 11:15 DoRon Motter, University of Michigan, USA (with Igor Markov)
On proof systems behind efficient SAT solvers
11:15 - 11:40 Gábor Kusper, Research Institute for Symbolic Computation, Linz, Austria
Solving the resolution-free SAT problem by hyper-unit propagation in linear time
11:40 - 12:05 Steven Prestwich, Cork Constraint Computation Center, Ireland (with Stéphane Bressan)
A SAT approach to query optimization in mediator systems
12:05 - 01:30 Lunch
01:30 - 01:55 Fahiem Bacchus, University of Toronto, Canada
Exploring the computational tradeoff of more reasoning and less searching
01:55 - 02:20 Chu Min Li, University of Picardie Jules Verne, France (with Hachemi Bennaceur)
An empirical measure for characterizing 3-SAT
02:20 - 02:45 Uwe Egly, Technische Universität, Austria (with Stefan Woltran and Reinhard Pichler)
On deciding subsumption problems
02:45 - 03:10 Fadi A. Aloul, University of Michigan, USA (with Arathi Ramani, Igor Markov, and Karem Sakallah)
PBS: A backtrack-search psuedo-Boolean solver and optimizer
03:10 - 03:25 Coffee Break
Quantified Boolean Formulas Mini Workshop II
03:25 - 03:55 Panel (Toby Walsh, Ian Gent, Hans Kleine Büning, Enrico Giunchiglia)
What QBF can learn from SAT (and vice versa)
03:55 - 04:20 Enrico Giunchiglia, Università degli Studi di Genova, Italy (with Massimo Narizzano, Armando Tacchella)
Assessing the impact of learning techniques in quantified Boolean logic satisfiability
04:20 - 04:45 Stefan Woltran, Technische Universität, Austria (with H. Tompits and Uwe Egly)
On quantifier shifting for quantified Boolean formulas
04:45 - 05:10 Hans Kleine Büning, Universität Paderborn, Germany (with Xishun Zhao)
Minimal falsity for QBF with deficiency 1
06:00 - 10:00 Dinner, Conference Center

Thursday, 9 May

08:05 - 08:30 Edward Hirsch, Steklov Institute of Mathematics at St. Petersburg, Russia (with Arist Kojevnikov)
UnitWalk: A new SAT solver that uses local search guided by unit clause elimination
08:30 - 08:55 Hantao Zhang, University of Iowa, USA
Generating college conference basketball schedules by a SAT solver
08:55 - 09:20 Yoichi Takenaka, Osaka University, Japan (with Akihiro Hashimoto)
An analog algorithm for the satisfiability problem
09:20 - 09:45 Holger Hoos, University of British Columbia, Canada
SLS algorithms for SAT: irregular instances, search stagnation, and mixture models
09:45 - 10:10 Felip Manya, Universitat de Lleida, Spain (with Carlos Ansótegui, Ramón Béjar, Alba Cabiscol, and Chu Min Li)
Resolution methods for many-valued CNF formulas
10:10 - 10:30    Coffee Break
10:30 - 10:55 Xishun Zhao, Zhongshan University, P.R. China (with Hans Kleine Büning)
Extension and equivalence problems for clause minimal formulas
10:55 - 11:20 Inna Davydova, St. Petersburg State University, Russia (with Gennady Davydov)
CNF application in discrete optimization
11:20 - 11:45 Sean Forman, St. Joseph's University, USA (with Alberto M. Segre)
NAGSAT: A randomized, complete, parallel solver for 3-SAT
11:45 - 12:10    Lyndon Drake, University of York, United Kingdom (with Alan Frisch and Toby Walsh)
Adding resolution to the DPLL procedure for satisfiability
12:10 - 01:30 Lunch featuring results of SAT competition and prizes
01:30 - 02:30 SAT Solver competition statistics and anything noteworthy learned
02:30 - 10:00 End of Conference