SAT 2008 -
Eleventh International Conference on
Theory and Applications of Satisfiability Testing
May 12 - 15 2008, Guangzhou, P. R. China
Preliminary Conference Program
Sunday, May 11
| 10:00 - 20:00 | Conference Registration |
| 18:00 - 20:00 | SAT Reception |
Monday, May 12
| 8:00 - | Conference Registration Open |
| 9:00 - 9:30 | Opening Ceremony |
| 9:30 - 10:30 | Session 1 |
| 9:30 | Searching for Autarkies to Trim Unsatisfiable Clause Sets |
| Mark Liffiton and Karem Sakallah | |
| 10:00 | Improvements to Hybrid Incremental SAT Algorithms |
| Florian Letombe and Joao Marques-Silva | |
| 10:30 - 11:00 | Coffee Break |
| 11:00 - 12:00 | Session 2 |
| 11:00 | Finding Guaranteed MUSes Fast |
| Hans van Maaren and Siert Wieringa | |
| 11:30 | Complexity and Algorithms for Well-Structured k-SAT Instances |
| Konstantinos Georgiou and Periklis A. Papakonstantinou | |
| 12:00 - 14:00 | Lunch |
| 14:00 - 16:00 | Session 3 |
| 14:00 | Random Instances of W[2]-Complete Problems: Thresholds, Complexity, and Algorithms |
| Yong Gao | |
| 14:30 | A Generalized Framework for Conflict Analysis |
| G. Audemard, L. Bordeaux, Y. Hamadi, S. Jabbour, and L. Sais | |
| 14:50 | Adaptive Restart Strategies for Conflict Driven SAT Solvers |
| Armin Biere | |
| 15:10 | Local Restarts |
| Vadim Ryvchin and Ofer Strichman | |
| 15:30 - 16:00 | Coffee Break |
| 16:00 - 17:00 | Session 4 |
| 16:00 | Designing an Efficient Hardware Implication Accelerator for SAT Solving |
| John Davis, Zhangxi Tan, Fang Yu, and Lintao Zhang | |
| 16:30 | Attacking Bivium Using SAT Solvers |
| Tobias Eibach, Enrico Pilz, and Gunnar Völkel | |
| 17:30 - 19:30 | Dinner |
| 20:00 - 22:00 | Boat Trip |
Tuesday, May 13
| 9:00 - 10:00 | Invited Talk |
| SAT, UNSAT and Coloring | |
| Kazuo Iwama | |
| 10:00 - 10:30 | Coffee Break |
| 10:30 - 12:00 | Session 5 |
| 10:30 | New Results on the Phase Transition for Random Quantified Boolean Formulas |
| Nadia Creignou, Hervé Daudé, Uwe Egly, and Raphaël Rossignol | |
| 11:00 | Nenofex: Expanding NNF for QBF Solving |
| Florian Lonsing and Armin Biere | |
| 11:30 | A CNF Class Generalizing Exact Linear Formulas |
| Stefan Porschen and Ewald Speckenmeyer | |
| 12:00 - 14:20 | Lunch |
| 14:20 - 16:00 | Session 6 |
| 14:20 | Modelling Max-CSP as Partial Max-SAT |
| Josep Argelich, Alba Cabiscol, Inęs Lynce, and Felip Manyŕ | |
| 14:50 | A Max-SAT Inference-Based Pre-processing for Max-Clique |
| Federico Heras and Javier Larrosa | |
| 15:20 | A Preprocessor for Max-SAT Solvers |
| Josep Argelich, Chu Min Li, and Felip Manyŕ | |
| 15:40 | Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms |
| Joao Marques-Silva and Vasco Manquinho | |
| 16:00 - 16:30 | Coffee Break |
| 16:30 - 17:30 | Session 7 |
| 16:30 | A Decision-Making Procedure for Resolution-Based SAT-Solvers |
| Eugene Goldberg | |
| 17:00 | Speeding-Up Non-clausal Local Search for Propositional Satisfiability with Clause Learning |
| Zbigniew Stachniak and Anton Belov | |
| 17:30 - 18:30 | Poster Session |
| 19:00 | Conference Banquet |
Wednesday, May 14
| 9:00 - 10:00 | Invited Talk |
| Regular and General Resolution: An Improved Separation | |
| Alasdair Urquhart | |
| 10:00 - 10:30 | Coffee Break |
| 10:30 - 11:30 | Session 8 |
| 10:30 | SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers |
| Germain Faure, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonel | |
| 11:00 | SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions |
| Maarten Mariën, Johan Wittocx, Marc Denecker, and Maurice Bruynooghe | |
| 12:00 - 14:00 | Lunch |
| 14:00 - 20:00 | Social Program |
| 20:00 - 21:00 | SAT Business Meeting |
Thursday, May 15
| 9:00 - 10:30 | Session 9 |
| 9:00 | SAT Competition |
| 9:30 | QBF Evaluation |
| 10:00 | MAX-SAT Evaluation |
| 10:30 - 11:00 | Coffee Break |
| 11:00 - 11:50 | Session 10 |
| 11:00 | The OKlibrary: A generative research platform for (generalised) SAT solving |
| (Additional Presentation) | |
| Oliver Kullmann | |
| 11:30 | Online Estimation of SAT Solving Runtime |
| Shai Haim and Toby Walsh | |
| 12:00 - 14:00 | Lunch |
| 14:00 - 15:30 | Session 11 |
| 14:00 | How Many Conflicts Does It Need to Be Unsatisfiable? |
| Dominik Scheder and Philipp Zumstein | |
| 14:30 | Computation of Renameable Horn Backdoors |
| Stephan Kottler, Michael Kaufmann, and Carsten Sinz | |
| 14:50 | A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors |
| Stephan Kottler, Michael Kaufmann, and Carsten Sinz | |
| 15:10 | CNF Encoding for Adjacencies in Boolean Cardinality Constraint |
| (Additional Presentation) | |
| Sachoun Park and Gihwon Kwon | |
| 15:30 - 16:30 | Coffee Break and Poster Session |
| 16:30 | End of Conference |
| (18:00 - 20:00) | Dinner |
(Long paper presentations: 30 minutes talk including discussion; short paper presentations: 20 minutes.)