Monday, 10 May 2004

08:00-09:00 Breakfast (provided @ Foyer)
09:00-09:20 Opening
09:20-10:10 Session 1 [Hard instances]

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

10:10-10:50 Coffee Break
10:50-12:30 Session 2 [SAT Solvers]

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

12:30-14:20 Lunch (provided @ Vistas 19th Floor)
14:20-15:20 Invited Talk
The Behavior of SAT Solvers in Model Checking Application
Ken McMillan, Cadence Berkeley Labs
15:20-15:50 Coffee Break (registration)
15:50-16:40 Session 3 [Algorithms & Bounds I]

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]

16:40-18:00 SAT Solvers Competition & QBF Solvers Evaluation
Competitions and results presented by Daniel Le Berre and Armando Tacchella
Panel discussion - panelists: Dave Tompkins, Armin Biere, João Marques Silva, Enrico Giunchiglia, Laurent Simon


Tuesday, 11 May 2004

08:00-09:00 Breakfast (provided @ Foyer)
09:00 - 10:15 Session 4 [Algorithms & Bounds II]

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

10:15-10:50 Coffee Break (registration)
10:50-12:30 Session 5 [Properties of Formulae / Non-Boolean Problems]

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

12:30-14:20 Lunch (provided @ Vistas 19th Floor)
14:20-15:20 Poster Overview Session I

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

15:20-16:20 Poster Session I (coffee provided)
16:20-18:00 Session 6 [Non-CNF SAT I]

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

Wednesday, 12 May 2004

08:00-09:00 Breakfast (provided @ Foyer)
09:00-10:15 Invited Talk
From Satisfiability to Proof Complexity and Bounded Arithmetic
Stephen Cook, University of Toronto
10:15-10:50 Coffee Break (registration)
10:50-12:30 Session 7 [Non-CNF SAT II]

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

12:30-14:30 Lunch (provided @ Vistas 19th Floor)
14:30-00:30 Excursion and Banquet

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

Thursday, 13 May 2004

08:00-09:25 Breakfast (provided @ Foyer) - note changed time!
09:25-10:15 Session 8 [Bounded Model Checking] - note changed time!

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

10:15-10:50 Coffee Break (registration)
10:50-12:30 Session 9 [QBF]

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

12:30-14:20 Lunch (provided @ Vistas 19th Floor)
14:20-15:20 Poster Overview Session II

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]

15:20-16:20 Poster Session II (coffee provided)