| 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 |
|
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).
|
| 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 |
| |
| 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 |
| |