|
没有相关文章 |
|
 |
|
 |
|
|
 |
|
SAT08 Preliminary Conference Program |
|
|
| SAT08 Preliminary Conference Program |
|
作者：佚名 文章来源：本站原创 点击数： 更新时间：2008-5-13 |
|
|
SAT08 Preliminary Conference Program
Sunday, May 11 (Lobby)
|
10:00 - 20:00 |
Conference Registration |
|
18:00 - 20:00 |
SAT Reception |
Monday, May 12 (Laiyin He Hall, the 4th Floor)
|
8:00 - |
Conference Registration Open |
|
9:00 - 9:30 |
Opening Ceremony |
|
|
|
|
9:30 - 10:30 |
Session 1 Chair : John Franco |
|
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 Chair: Uwe Egly |
|
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 Chair: Chumin Li |
|
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 Chair: Armin Biere |
|
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 (Hongyun Hall, the 3rd Floor)
|
9:00 - 10:00 |
Invited Talk Chair |
|
|
SAT, UNSAT and Coloring |
|
|
Kazuo Iwama |
|
|
|
|
10:00 - 10:30 |
Coffee Break |
|
|
|
|
10:30 - 12:00 |
Session 5 Chair: Eugene Goldberg |
|
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 Chair: Jian Zhang |
|
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 Chair: Oliver Kullmann |
|
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 (Hongyun Hall, the 3rd Floor)
|
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 Chair: Nadia Creignou |
|
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 (Hongyun Hall, the 3rd Floor) |
Thursday, May 15 (Hongyun Hall, the 3rd Floor)
|
9:00 - 10:30 |
Session 9 Chair: Joao Marques-Silva |
|
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 Chair: Lintao Zhang |
|
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 Chair: Karem Sakallah |
|
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 |
| | |
您现在的位置：