| SAT06 | 9th International Conference on Theory and Applications of Satisfiability Testing Seattle, August 12 - 15, 2006 |
Program
Friday, August 11th
Friday's program is also available side by side with other meetings.
19:00‑21:00 SAT Reception
Location:
Grand Ballroom B
Saturday, August 12th
Saturday's program is also available with abstracts or side by side with other meetings.
08:45‑10:00 FLoC Opening and Plenary Session
Chair:
Moshe Vardi, Thomas Ball, Wolfram Schulte, Rajeev Alur
Location:
Grand Ballroom C
| 08:45 | Introduction and Welcome |
| 09:00 | Randal E. Bryant
(Carnegie Mellon University) Formal Verification of Infinite State Systems using Boolean Methods [ppt] |
10:00‑10:30 Break
10:30‑12:30 Session 1: Proofs and Cores
Chair:
Sharad Malik
Location:
Grand Ballroom D
12:30‑14:00 Lunch break
14:00‑15:30 Session 2: Heuristics and Algorithms
Chair:
Inęs Lynce
Location:
Grand Ballroom D
| 14:00 | Mark Chavira and Adnan Darwiche Pre-Processing CNFs to Enhance Component Analysis |
| 14:30 | Himanshu Jain
, Constantinos Bartzis and Edmund Clarke Satisfiability Checking of Non-clausal Formulas using General Matings |
| 15:00 | Eugene Goldberg
Determinization of resolution by an algorithm operating on complete assignments |
| 15:15 | Hantao Zhang A Complete Random Jump Strategy with Guiding Paths |
15:30‑16:00 Break
16:00‑17:30 Session 3: Applications
Chair:
Miroslav Velev
Location:
Grand Ballroom D
| 16:00 | Ilya Mironov and Lintao Zhang
Applications of SAT-Solvers to Cryptanalysis |
| 16:30 | Yuliya Zabiyaka and Adnan Darwiche Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies |
| 17:00 | Roberto Sebastiani
and Michele Vescovi Encoding the satisfiability of modal and description logics into SAT: the case study of K(m)/ALC |
| 17:15 | Ines Lynce
and Joao Marques-Silva
SAT in Bioinformatics: Making the Case with Haplotype Inference |
18:00‑20:00 SAT Business Meeting
Location:
Richmond (4th floor)
Sunday, August 13th
Sunday's program is also available with abstracts or side by side with other meetings.
09:00‑10:00 Invited Talk
Chair:
Armin Biere
Location:
Grand Ballroom D
| 09:00 | Karem Sakallah
(University of Michigan, Ann Arbor) From Propositional Satisfiability To Satisfiability Modulo Theories [ppt] |
10:00‑10:30 Break
10:30‑12:30 Session 4: SMT
Chair:
Alessandro Cimatti
Location:
Grand Ballroom D
| 10:30 | Yinlei Yu and Sharad Malik
Lemma Learning in SMT on Linear Constraints |
| 11:00 | Robert Nieuwenhuis
and Albert Oliveras
On SAT Modulo Theories and Optimization Problems |
| 11:30 | Scott Cotton and Oded Maler Fast and Flexible Difference Constraint Propagation for DPLL(T) |
| 12:00 | Hossein Sheini
and Karem Sakallah
A Progressive Simplifier for Satisfiability Modulo Theories |
12:30‑14:00 Lunch break
14:00‑15:30 Session 5: Structure
Chair:
Stefan Szeider
Location:
Grand Ballroom D
| 14:00 | Uwe Bubeck
and Hans Kleine Büning
Dependency Quantified Horn Formulas: Models and Complexity |
| 14:30 | Stefan Porschen, Ewald Speckenmeyer and Bert Randerath On Linear CNF Formulas |
| 15:00 | Su Chen, Tomasz Imielinski, Karin Johnsgard, Donald Smith and Mario Szegedy A Dichotomy Theorem for Constraint Satisfaction Problems with Disjoint Domains |
15:30‑16:00 Break
16:00‑18:00 Poster Session
Location:
Grand Ballroom D
19:00‑22:00 LICS-SAT-RTA Joint Banquet
Location:
Grand Ballroom B
Monday, August 14th
Monday's program is also available with abstracts or side by side with other meetings.
09:00‑10:00 Invited Talk
Chair:
Carla P. Gomes
Location:
Metropolitan B
| 09:00 | Fahiem Bacchus
(University of Toronto, Canada) CSPs: Adding Structure to SAT [ppt] |
10:00‑10:30 Break
10:30‑12:30 Session 6: MAX-SAT
Chair:
Ewald Speckenmeyer
Location:
Metropolitan B
12:30‑14:00 Lunch break
14:00‑16:00 Session 7: Local Search and Survey Propagation
Chair:
Hans van Maaren
Location:
Metropolitan B
| 14:00 | Steven Prestwich and Ines Lynce
Local Search for Unsatisfiability |
| 14:30 | Andrei Bulatov
and Evgeny Skvortsov Efficiency of Local Search |
| 15:00 | Panagiotis Manolios
and Yimin Zhang Implementing Survey Propagation on Graphics Processing Units |
| 15:30 | Eric Hsu
and Sheila McIlraith Characterizing Propagation Methods for Boolean Satisfiability |
16:00‑16:30 Break
16:30‑18:00 Keynote Session: Marking the Gödel Centenary
Chair:
Wolfram Schulte, Moshe Vardi
Location:
Metropolitan A and B
| 16:30 | John Dawson
(Penn State, York Campus) Shaken Foundations or Groundbreaking Realignment? A Centennial Assessment of Kurt Gödel's Impact on Logic, Mathematics, and Computer Science [ppt] |
| 17:15 | Dana Scott
(Carnegie Mellon University) The Future of Proof [pdf] |
Tuesday, August 15th
Tuesday's program is also available with abstracts or side by side with other meetings.
09:00‑10:00 Competitions
Chair:
Joăo Marques-Silva
Location:
Metropolitan B
| 09:00 | Carsten Sinz
SAT-Race |
| 09:20 | Olivier Roussel
Pseudo Boolean Evaluation |
| 09:40 | Armando Tacchella
QBF Evaluation |
10:00‑10:30 Break
10:30‑12:30 Session 8: QBF
Chair:
Lintao Zhang
Location:
Metropolitan B
| 10:30 | Hans Kleine Büning
and Xishun Zhao
Minimal False Quantified Boolean Formulas |
| 11:00 | Horst Samulowitz
and Fahiem Bacchus
Binary Clause Reasoning in QBF |
| 11:30 | Daijue Tang and Sharad Malik
Solving Quantified Boolean Formulas with Circuit Observability Don't Cares |
| 12:00 | Ashish Sabharwal
, Carlos Ansotegui, Carla P. Gomes
, Justin W. Hart
and Bart Selman
QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency |
12:30‑14:00 Lunch break
14:00‑15:30 Session 9: Counting and Concurrency
Chair:
Ashish Sabharwal
Location:
Metropolitan B
| 14:00 | Naomi Nishimura
, Prabhakar Ragde
and Stefan Szeider
Solving #SAT using Vertex Covers |
| 14:30 | António Morgado, Paulo Matos
, Vasco Manquinho and Joao Marques-Silva
Counting Models in Integer Domains |
| 15:00 | Marc Thurley sharpSAT - counting models with advanced component caching and implicit BCP |
| 15:15 | Antti Eero Johannes Hyvärinen, Tommi Junttila and Ilkka Niemelä A Distribution Method for Solving SAT in Grids |
15:30‑16:00 Break
16:00‑18:00 Poster Session
Location:
Metropolitan B
