SAT 2007 - Tenth International Conference on
Theory and Applications of Satisfiability Testing

May 28 - 31 2007, Lisbon, Portugal

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