| 09.45 - 10.00 | Opening Address |
| 10.00 - 10.45 |
Thomas Eiter, Toshihide Ibaraki, Kazuhisa Makino On Satisfiability of Partially Defined Double and Bidual Horn Functions |
| 10.45 - 11.15 | Coffee Break |
| 11.15 - 12.00 |
Paul Purdom Probe Order Backtracking |
| 12.00 - 12.45 |
Hans Kleine Buening, Theodor Lettmenn Resolution Remains Hard Under Equivalence |
| 12.45 - 14.30 | Lunch |
| 14.30 - 15.15 |
Alasdair Urquhart The Symmetry Rule in Propositional Logic |
| 20.00 | Dinner |
| 9.15 - 10.00 |
Peter Heusch, Marc-Andre Lemburg, Ewald Speckenmeyer Complexity Results of Subclasses of the Pure Implicational Calculus |
| 10.00 - 10.45 |
John Franco, Judy Goldsmith, John Schlipf, Ewald Speckenmeyer, R. Swaminathan An Algorithm for the class of Pure Implicational Formulas |
| 10.45 - 11.15 | Coffee Break |
| 11.15 - 12.00 |
Jinchang Wang Testing Propositional Satisfiability by Using Binary Trees |
| 12.00 - 12.45 |
Ingo Schiermeyer Pure Literal Look Ahead: An O(1.479^n) 3-Satisfiability Algorithm |
| 12.45 - 14.30 | Lunch |
| 14.30 - 15.15 |
Allen Van Gelder, Fumiaki Kamiya Lemma and Cut Strategies for Two-Sided Propositional Resolution |
| 15.15 - 16.00 |
Oliver Kullmann Blocked Clauses; Their Use for SAT Decision, And An Analysis of Their Strength |
| 20.00 | Dinner |
|
09.15 |
Hans Kleine Buening, Theodor Lettmann Closure Under Replacements Versus Run Time of the Davis-Putnam Algorithms and Distribution of Satisfiable Formulas |
|
10.00 |
Hans Van Maaren Discriminative Properties of the Smooth Convex Quadratic Approximation of a 3-SAT Problem |
|
10.45 |
Coffee Break |
|
11.15 |
Jun Gu Multi-SAT Algorithm |
|
12.00 |
Marco Protassi MAX-SAT and the Class APX |
|
09.15 |
Paolo Nobili, Antonio Sassano Strengthening Lagrangian Bounds for the MAX-SAT Problem |
| 10.00 - 10.45 |
Giorgio Gallo, C. Gentile, D. Pretolani MAX Horn SAT and Directed Hypergraphs: Algorithmic Enhancements and Easy Cases |
|
10.45 |
Coffee Break |
| 11.15 - 12.00 |
Roberto Battiti, Marco Protassi Reactive Search: A History-Based Heuristic for MAX-SAT |
| 12.00 - 12.45 |
Endre Boros On Maximum Renamable Horn Sub-CNFs |
| 12.45 - 14.30 | Lunch |
| 14.30 - 15.15 |
Andreas Goerdt Probability of Satisfiability of Random 2-SAT Instances with Quantification |
| 15.15 - 16.00 |
David Mitchell Toward an Adequate SAT Algorithm |
| 10.00 - 11.00 | Open Problems I |
|
11.00 |
Coffee Break |
| 11.30 - 12.30 | Open Problems II |