Top
News
Slides
Photos
Venue
Invited Speakers
Final Program
Committees
Important Dates
Competitions
JSAT Special Issue
Conference Location
Conference Registration
Hotel Reservations
Flying with TAP
Paper Submissions
Sponsors
Previous Conferences
|
Conference Program
Sunday, May 27
18:00‑21:00 Conference Registration
19:00‑21:00 SAT Reception
Monday, May 28
08:30‑ Conference Registration Open
09:00‑09:30 Introduction and Welcome
09:30‑10:30 Session 1: Encodings
Chair: Steven Prestwich
| 09:30 |
P. Manolios and D. Vroon
Efficient Circuit to CNF Conversion
|
| 09:45 |
C. Ansótegui Gil, M. L. Bonet, J. Levy and F. Manyà
Mapping CSP into Many-Valued SAT
|
| 10:00 |
G. Audemard and L. Sais
Circuit Based Encoding for CNF formulas
|
| 10:15 |
I. Lynce and J. Marques-Silva
Breaking Symmetries in SAT Matrix Models
|
10:30‑11:00 Coffee break
11:00‑12:30 Session 2: Max-SAT and Pseudo-Boolean
Chair: Fahiem Bacchus
| 11:00 |
J. Argelich and F. Manyà
Partial Max-SAT Solvers with Clause Learning
|
| 11:30 |
F. Heras, J. Larrosa and A. Oliveras
MiniMaxSat: a New Weighted Max-SAT Solver
|
| 12:00 |
M. Lukasiewycz, M. Glass, C. Haubelt and J. Teich
Solving Multi-Objective Pseudo-Boolean Problems
|
12:30‑14:00 Lunch break
14:00‑15:30 Session 3: Structure I
Chair: Oliver Kullmann
| 14:00 |
A. Kojevnikov
Improved Lower Bounds for Tree-Like Resolution over Linear Inequalities
|
| 14:30 |
M. Langlois, R. Sloan and G. Turan
Horn Upper Bounds and Renaming
|
| 15:00 |
S. Szeider
Matched Formulas and Backdoor Sets
|
| 15:15 |
C. Gomes, J. Hoffmann, A. Sabharwal and B. Selman
Short XORs for Model Counting: From Theory to Practice
|
15:30‑16:00 Coffee break
16:00‑17:30 Session 4: Local Search
Chair: Anbulagan
| 16:00 |
S. Prestwich
Variable Dependency in Local Search: Prevention is Better than
Cure
|
| 16:30 |
C.-M. Li, W. Wei and H. Zhang
Combining Adaptive Noise and Look-Ahead in Local Search for
SAT
|
| 17:00 |
M. Heule and H. van Maaren
From Idempotent Generalized Boolean Assignments to Multi-Bit Search
|
17:30‑19:00 SAT Business Meeting
Tuesday, May 29
09:00‑10:00 Invited Talk
Chair: Karem Sakallah
| 09:00 |
Martin Davis, SAT: Past and future
|
10:00‑10:30 Coffee break
10:30‑12:30 Session 5: Structure II
Chair: Stefan Szeider
| 10:30 |
D. Scheder and P. Zumstein
Satisfiability with Exponential Families
|
| 11:00 |
A. Hertel, P. Hertel and A. Urquhart
Formalizing Dangerous SAT Encodings
|
| 11:30 |
S. Porschen and E. Speckenmeyer
Algorithms for Variable-Weighted 2-SAT and Dual Problems
|
| 12:00 |
K. Makino, S. Tamaki and M. Yamamoto
On the Boolean Connectivity Problem for Horn Relations
|
12:30‑14:00 Lunch break
14:00‑18:00 Social Programme: Sightseeing in Sintra and Cascais
Wednesday, May 30
09:00‑10:00 Invited Talk
Chair: Joao Marques-Silva
| 09:00 |
Andrei Voronkov, Encodings of Problems in Effectively Propositional Logic
|
10:00‑10:30 Coffee break
10:30‑12:30 Session 6: QBF
Chair: Armando Tacchella
| 10:30 |
T. Jussila, A. Biere, C. Sinz, D. Kroening and
C. Wintersteiger
A First Step Towards a Unified Proof Checker for QBF
|
| 11:00 |
H. Samulowitz and F. Bacchus
Dynamically Partitioning for Solving QBF
|
| 11:30 |
M. Samer and S. Szeider
Backdoor Sets of Quantified Boolean Formulas
|
| 12:00 |
U. Bubeck and H. Kleine Buning
Bounded Universal Expansion for Preprocessing QBF
|
12:30‑14:00 Lunch break
14:00‑15:30 Session 7: Complete Algorithms
Chair: Allen Van Gelder
| 14:00 |
M. Heule and H. van Maaren
Effective Incorporation of Double Look-Ahead Procedures
|
| 14:30 |
N. Een, N. Sorensson and A. Mishchenko
Applying Logic Synthesis for Speeding Up SAT
|
| 15:00 |
A. Nadel, N. Dershowitz and Z. Hanna
Towards a Better Understanding of the Functionality of a
Conflict-Driven SAT Solver
|
| 15:15 |
K. Pipatsrisawat and A. Darwiche
A Lightweight Component Caching Scheme for Satisfiability Solvers
|
15:30‑16:00 Coffee break
16:00‑17:30 Session 8: Proofs and Cores
Chair: Hans van Maaren
| 16:00 |
J. Buresh-Oppenheim and D. Mitchell
Minimum 2CNF Resolution Refutations in Polynomial Time
|
| 16:30 |
O. Kullmann
Polynomial Time SAT Decision for Complementation-invariant
Clause-sets, and Sign-non-singular Matrices
|
| 17:00 |
A. Van Gelder
Verifying Propositional Unsatisfiability: Pitfalls to Avoid
|
| 17:15 |
A. Cimatti, A. Griggio and R. Sebastiani
A Simple and Flexible Way of Computing Small Unsatifiable
Cores in SAT Modulo Theories
|
19:30‑22:30 Social Programme: Conference Banquet
Thursday, May 31
09:00‑10:30 Session 9: Applications
Chair: Panagiotis Manolios
| 09:00 |
C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp,
R. Thiemann and H. Zankl
SAT Solving for Termination Analysis with Polynomial
Interpretations
|
| 09:30 |
S. Staber and R. Bloem
Fault Localization and Correction with QBF
|
| 10:00 |
F. Aloul and N. Kandasamy
Sensor Deployment for Failure Diagnosis in Networked Aerial
Robots: A Satisfiability-Based Approach
|
| 10:15 |
D. De, A. Kumarasubramanian and R. Venkatesan
Inversion Attacks on Secure Hash Functions using SAT Solvers
|
10:30‑11:00 Coffee break and Poster session
11:00‑12:30 Session 10: Competitions and Evaluations
Chair: Armin Biere
| 11:00 |
QBF Evaluation
|
| 11:20 |
PB Evaluation
|
| 11:40 |
Max-SAT Evaluation
|
| 12:00 |
SAT Competition
|
12:30‑14:00 Lunch break
14:00‑16:00 Special Session on Modern SAT Solving
Chair: John Franco
| 14:00 |
Invited Talk
Armin Biere, A Short History of SAT Solver Technology and
What is Next?
|
| 15:00 |
Tobias Schubert, Multi-Threaded SAT Solving
|
| 15:30 |
Q&A on the 2007 Best Performing Solvers
|
16:00‑17:00 Coffee break and Poster session
17:00 End of Conference
|
