18:00-19:30 |
Registration Desk |
MONDAY, MAY 5 TH |
||
8:00-8:55 |
Registration Desk |
|
8:55-9:20 |
Hans Kleine Büning, Zhao Xishun |
Read-Once Unit Resolution |
9:20-9:55 |
Stefan Porschen, Bert Randerath, Ewald Speckenmeyer |
Linear Time Algorithms for some Not-all-Equal Satisfiability Problems |
9:55-10:20 |
Nadia Creignou, Hervé Daudé |
Crossed classification, complexity versus phase transition, for Boolean CSPs |
10:20-10:50 |
Coffee Break |
|
10:50-11:15 |
Hubie Chen |
An Algorithm for SAT Above the Threshold |
11:15-11:40 |
Ryan Williams |
On Computing k-CNF Formula Properties |
11:40-12:05 |
Sven Baumer, Rainer Schuler |
Improving a probabilistic 3-SAT Algorithm by Dynamic Search and Independent Clause Pairs |
12:05-12:30 |
Oliver Kullmann |
On some connections between linear algebra and the combinatorics of clause-sets |
12:30-14:00 |
Lunch |
|
14:00- 15:00 |
Invited speaker: Riccardo Zecchina |
Survey Propagation: from analytic results on random k-sat to a message-passing algorithm for satisfiability |
15:00-15:25 |
Giorgio Parisi |
On the probabilistic approach to the random satisfiability problem |
15:25-15:50 |
Guilhem Semerjian, Remi Monasson |
A study of Pure Random Walk on Random Satisfiability Problems with physical methods |
15:50-16:15 |
Hans van Maaren, Linda van Norden |
Hidden threshold phenomena for fixed-density SAT-formulae |
16:15-16:45 |
Coffee Break |
|
16:45-17:10 |
Stefan Szeider |
On fixed-parameter tractable parameterizations of SAT |
17:10-17:35 |
Daniele Pretolani |
Satisfiability Problems in Partial 2-hypertrees |
17:35-18:00 |
Youichi Hanatani, Takashi Horiyama, Kazuo Iwama |
Density Condensation of Boolean Formulas |
18:00-18:25 |
Eugene Goldberg, Yakov Novikov |
How good are current resolution based SAT-solvers? |
19.30 |
Welcome Reception |
TUESDAY, MAY 6 TH |
||
8:30-9:30 |
Invited speaker: Toby Walsh |
Challenges in SAT (and QBF) |
9:30-9:55 |
J.Franco, M.Kouril, J.Schlipf, J.Ward, S.Weaver, M.Dransfield, W.M.Vanfleet |
SBSAT: A State-Based, BDD-Based Satisfiability Solver |
9:55-10:20 |
Ashish Sabharwal, Paul Beame, Henry Kautz |
Using Problem Structure for Efficient Clause Learning |
10:20-10:50 |
Coffee Break |
|
10:50-11:15 |
Marc Herbstritt, Bernd Becker |
Conflict-based Selection of Branching Rules |
11:15-11:40 |
Lyndon Drake, Alan Frisch |
The Interaction Between Inference and Branching Heuristics |
11:40-12:05 |
Fahiem Bacchus, Jonathan Winter |
Effective Preprocessing with Hyper-Resolution and Equality Reduction |
12:05-12:30 |
Lintao Zhang, Sharad Malik |
Cache Performance of SAT Solvers: A Case Study for Efficient Implementation of Algorithms |
12:30-12:55 |
Paolo Liberatore |
Algorithms and Experiments on Finding Minimal Models |
12:55-14:25 |
Lunch |
|
14:25-14:50 |
Enrico Giunchiglia, Marco Maratea, Armando Tacchella |
Look-Ahead vs. Look-Back Techniques in a Modern SAT Solver |
14:50-15:15 |
Ryan Williams, Carla Gomes, Bart Selman |
On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search |
15:15-15:40 |
Yannet Interian |
Backdoor sets for random 3-SAT |
15:40-16:05 |
Lintao Zhang, Sharad Malik |
Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formula |
16:05-16:35 |
Per Bjesse, James Kukula, Robert Damiano, Ted Stanion, Yunshan Zhu |
Guiding SAT Diagnosis with Tree Decompositions |
16:35- |
Poster Session |
WEDNESDAY, MAY 7 TH |
||
8:30-8:55 |
Franc Brglez, Matthias F. Stallmann, Xiao Yu Li |
SATbed: An Environment For Reliable Performance Experiments with SAT Instance Classes and Algorithms |
8:55-12:30 |
Solvers presentation and Competition/Evaluation results: |
|
1) Presentation of SAT solvers participating to the competition |
||
2) Presentation of the results + awards |
||
3) Presentation of the QBF solvers participating the evaluation |
||
4) Presentation of the results |
||
5) Discussion about the next SAT/QBF competitions |
||
12:30-14:00 |
Lunch |
THURSDAY, MAY 8 TH |
||
8:30-9:30 |
Invited speaker: Wolfgang Kunz |
ATPG versus SAT: comparing two paradigms for Boolean reasoning |
9:30-9:55 |
Scott Diehl, Kevin Compton |
An implementation of the polynomial calculus as a SAT solver |
9:55-10:20 |
Renato Bruni |
Solving Error Correction for Large Data Sets as Propositional Satisfiability |
10:20-10:50 |
Coffee Break |
|
10:50-11:15 |
Alessandro Armando, Luca Compagna |
Automatic Analysis of Security Protocols via Reduction to SAT |
11:15-11:40 |
Elizabeth Broering, Satyanarayana V. Lokam |
Width-based Algorithms for SAT and CIRCUIT-SAT |
11:40-12:05 |
Edmund Clarke, Muralidhar Talupur, Dong Wang |
SAT based Predicate Abstraction for Hardware Verification |
12:05-12:30 |
Sarfraz Khurshid, Darko Marinov, Ilya Shlyakhter, Daniel Jackson |
A Case for Efficient Solution Enumeration |
12:30-14:00 |
Lunch |
|
14:00-14:25 |
Michael R. Dransfield, Victor W. Marek, Miroslaw Truszczynski |
Satisfiability and Computing van der Waerden numbers |
14:25-14:50 |
Hans Kleine Büning, K. Subramani, Xishun Zhao |
On Boolean Models for Quantified Boolean Horn Formulas |
14:50-15:15 |
Ian Gent, Enrico Giunchiglia, Massimo Narizzano, Andrew Rowley, Armando Tacchella |
Watched Data Structures for QBF Solvers |
15:15-15:40 |
Maher Mneimneh, Karem Sakallah |
Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution |
15:40-16:05 |
U. Egly, M. Seidl, H. Tompits, S. Woltran, M. Zolda |
Comparing Different Prenexing Strategies for Quantified Boolean Formulas |
16:05-16:35 |
Coffee Break |
|
16:35-17:00 |
Xiao Yu Li, Matthias F. Stallmann, Franc Brglez |
QingTing: A Fast SAT Solver Using Local Search and Efficient Unit Propagation |
17:00-17:25 |
Steven Prestwich |
Local Search on SAT-Encoded CSPs |
17:25-17:50 |
Christian Bessiere, Emmanuel Hebrard, Toby Walsh |
Local Consistencies in SAT |
17:50-18:15 |
Teresa Alsinet, Felip Manya, Jordi Planes |
Improved Branch and Bound Algorithms for Max-SAT |
POSTER PRESENTATIONS: |
|
Calin Anton, Joseph Culberson |
Generating Instances of Intermediate Hardness for Satisfiability |
Hui Xu, Rob A. Rutenbar |
Insights from Almost Satisfied: Quantifying the Fine-Structure of Unsatisfiability for 3-SAT Phase T |
Eduardo Rodriguez-Tello, Jose Torres-Jimenez |
SAT Solving Using a GA and an Epistasis Reducer Algorithm. |
Roland Yap, Stella Wang, Martin Henz |
Real-time Reconfigurable Hardware WSAT Variants |
M. Baioletti, A. Capotorti, S. Tulipani |
Procedures for the CPA problem based on the elimination of Boolean constraints |
Shlomit Bergman, Eliezer L. Lozinskii |
A Fast Algorithm for MAX-SAT Approximation |
James M. McQuillan, Craig A. Damon |
Random versus non-random 3-CNF expressions, 3-SAT, and Davis-Putnam |
Martin Fürer |
Forced Horn Satisfiability |
Ilya Shlyakhter, Manu Sridharan, Robert Seater, Daniel Jackson |
Exploiting Subformula Sharing in Automatic Analysis of Quantified Formulas |
Inês Lynce, João Marques-Silva |
On Implementing More Efficient SAT Data Structures |
Yimin Zhang, Hai Lin, JiGui Sun, DanTong Ou Yang |
Generating SAT Instances Using One-way Hash Function |
Zbigniew Lonc, Miroslaw Truszczynski |
Computing all models of CNF theories |
Sarah Ibri, Habiba Drias |
Parallel ACS for weighted MAX-SAT |
Gilles Audemard, Daniel Le Berre, Olivier Roussel, Inês Lynce, João Marques-Silva |
OpenSAT: An Open Source SAT Software Project |