• A Random Constraint Satisfaction Problem That Seems Hard for DPLL
Harold Connamacher

• From Spin Glasses to Hard Satisfiable Formulas
Haixia Jia, Cris Moore, and Bart Selman

• Combining Component Caching and Clause Learning for Effective Model Counting
Tian Sang, Fahiem Bacchus, Paul Beame, Henry Kautz, and Toniann Pitassi

• Early Conflict Detection Based BCP for SAT Solving
Matthew D.T. Lewis, Tobias Schubert, and Bernd W. Becker

• UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT & MAX-SAT
Dave A.D. Tompkins and Holger H. Hoos

• CirCUs: A Hybrid Satisfiability Solver
HoonSang Jin and Fabio Somenzi

• Computing Unsatisfiable k-SAT Instances with Few Occurrences per Variable
Shlomo Hoory and Stefan Szeider

• Algorithms for Satisfiability using Independent Sets of Variables
Ravi Gummadi, N.S. Narayanaswamy, and R. Venkatakrishnan
[the talk is given by Ramesh Krishnamurthy]

• Derandomization of Schuler's Algorithm for SAT
Evgeny Dantsin and Alexander Wolpert

• Polynomial Time SAT Decision, Hypergraph Transversals and the Hermitian Rank
Nicola Galesi and Oliver Kullmann

• Approximation Algorithm for Random MAX-kSAT
Yannet Interian

• Detecting Backdoor Sets with Respect to Horn and Binary Clauses
Naomi Nishimura, Prabhakar Ragde, and Stefan Szeider

• A Note on Satisfying Truth-Value Assignments of Boolean Formulas
Zbigniew Stachniak

• Mapping Problems with Finite-Domain Variables into Problems with Boolean Variables
Carlos Ansótegui and Felip Manyà

• Using Lower-Bound Estimates in SAT-Based Pseudo-Boolean Optimization
Vasco M. Manquinho and João Marques-Silva

• Worst Case Bounds for some NP-Complete Modified Horn-SAT Problems
Stefan Porschen and Ewald Speckenmeyer

• Satisfiability Threshold of the Skewed Random k-SAT
Danila A. Sinopalnikov

• Local Search for Very Large SAT Problems
Steven Prestwich and Colin Quirke

• Local Search with Bootstrapping
Lengning Liu and Miroslaw Truszczynski

• Efficient Implementations of SAT Local Search
Alex Fukunaga

• Adding a New Conflict Based Branching Heuristic in two Evolved DPLL SAT Solvers
Renato Bruni and Andrea Santori

• Using Rewarding Mechanisms for Improving Branching Heuristics
Elsa Carvalho and João Marques-Silva

• On Computing Minimum Unsatisfiable Cores
Ines Lynce and João Marques-Silva

• Visualizing the Internal Structure of SAT Instances
Carsten Sinz

• Using DPLL for Efficient OBDD Construction
Jinbo Huang and Adnan Darwiche

• Search vs. Symbolic Techniques in Satisfiability Solving
Guoqiang Pan and Moshe Y. Vardi

• Solving Non-clausal Formulas with DPLL search
Christian Thiffault, Fahiem Bacchus, and Toby Walsh

• Automatic Extraction of Functional Dependencies
Éric Grégoire, Richard Ostrowski, Bertrand Mazure, and Lakhdar Saïs

• A SAT-based Decision Procedure for the Boolean Combination of Difference Constraints
Alessandro Armando, Claudio Castellini, Enrico Giunchiglia, and Marco Maratea

• Aligning CNF- and Equivalence-reasoning
Marijn Heule and Hans van Maaren

• An Algebraic Approach to the Complexity of Generalized Conjunctive Queries
Michael Bauland, Philippe Chapdelaine, Nadia Creignou, Miki Hermann, and Heribert Vollmer

• A SAT Based Scheduler for Tournament Schedules
Hantao Zhang, Dapeng Li, and Haiou Shen

14:30 Group Leaves Hotel for Aquarium (by foot – meet in Foyer)

17:30 Bus Leaves Aquarium for Banquet 17:30 Bus Leaves Hotel for Banquet

19:30 Banquet Starts (Grouse Mountain)

~23:15 Skyride Leaves Mountain Top ~23:45 Skyride Leaves Mountain Top

• Incremental Compilation-to-SAT Procedures
Marco Benedetti and Sara Bernardini

• Analysis of Search Based Algorithms for Satisfiability of Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems
Daijue Tang, Yinlei Yu, Darsh Ranjan, and Sharad Malik

• Looking Algebraically at Tractable Quantified Boolean Formulas
Hubie Chen and Víctor Dalmau

• Equivalence Models for Quantified Boolean Formulas
Hans Kleine Büning and Xishun Zhao
Unfortunately, this talk was cancelled

• Encoding Global Unobservability for Efficient Translation to SAT
Miroslav N. Velev [presented by Daniel Le Berre]

• Resolve and Expand
Armin Biere

• QBF Reasoning on Real-World Instances
Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella

• A Comparative Study of 2QBF Algorithms
Darsh P. Ranjan, Daijue Tang, Sharad Malik

• Dealing with Symmetries in Quantified Boolean Formulas
Gilles Audemard, Bertrand Mazure and Lakhdar Saïs

• Improving First-order Model Searching by Propositional Reasoning and Lemma Learning
Zhuo Huang, Hantao Zhang, and Jian Zhang

• Boolean Ring Satisfiability
Nachum Dershowitz, Jieh Hsiang, Guan-Shieng Huang, and Daher Kaiss

• Game-SAT: A Preliminary Report
Ling Zhao and Martin Müeller

• Verifying the On-Line Help System of SIEMENS Magnetic Resonance Tomographs
Carsten Sinz and Wolfgang Küchlin

• NiVER: Non Increasing Variable Elimination Resolution for Preprocessing SAT instances
Sathiamoorthy Subbarayan and Dhiraj K Pradhan

• The Optimality of a Fast CNF Conversion and its Use with SAT
Daniel Sheridan

• Full CNF Encoding: The Counting Constraints Case
Olivier Bailleux and Yacine Boufkhad [presented by Lakhdar Sais]