SAT 2006

Program

[regular talks 30 minutes, short talks (marked '*') 15 minutes, incl. discussion]

----------------------------------------------------------------------------------
-- Friday, August 11 -------------------------------------------------------------
----------------------------------------------------------------------------------

19:00 - 21:00 Reception

----------------------------------------------------------------------------------
-- Saturday, August 12 -----------------------------------------------------------
----------------------------------------------------------------------------------

09:00 - 10:00 Plenary Talk 
  
  Randy Bryant.
  Formal Verification of Infinite State Systems using Boolean Methods.

10:00 - 10:30 Coffee

10:30 - 12:30 Proofs and Cores

  Arist Kojevnikov and Alexander S. Kulikov.
  Complexity of Semialgebraic Proofs with Restricted Degree of Falsity.

  Oliver Kullmann, Ines Lynce and Joao Marques-Silva.
  Categorisation of clauses in conjunctive normal forms:
  Minimally unsatisfiable sub-clause-sets and the lean kernel.

* Alexander Nadel, Nachum Dershowitz and Ziyad Hanna.
  A Scalable Algorithm for Minimal Unsatisfiable Core Extraction.

* Joshua Buresh-Oppenheim and David Mitchell.
  On the Exact Resolution Complexity of 2SAT.

* Allen Van Gelder.
  Input Cover Number as a Metric for Propositional Resolution Proofs.

* Toni Jussila, Carsten Sinz and Armin Biere.
  Extended Resolution Proofs for Symbolic SAT Solving with Quantification.

12:30 - 14:00 Lunch

14:00 - 15:30 Heuristics and Algorithms

  Mark Chavira and Adnan Darwiche.
  Pre-Processing CNFs to Enhance Component Analysis.

  Himanshu Jain, Constantinos Bartzis and Edmund Clarke.
  Satisfiability Checking of Non-clausal Formulae using General Matings.

* Eugene Goldberg.
  Determinization of resolution by an algorithm operating on complete assignments.

* Hantao Zhang.
  A Complete Random Jump Strategy with Guiding Paths.

15:30 - 16:00 Coffee

16:00 - 17:30 Applications

  Ilya Mironov and Lintao Zhang.
  Applications of SAT-Solvers to Cryptanalysis.

  Yuliya Zabiyaka and Adnan Darwiche.
  Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies.

* Roberto Sebastiani and Michele Vescovi.
  Encoding the satisfiability of modal and description logics into SAT: the case study of K(m)/ALC.

* Ines Lynce and Joao Marques-Silva.
  SAT in Bioinformatics: Making the Case with Haplotype Inference.

18:00 - 20:00 SAT Business Meeting

----------------------------------------------------------------------------------
-- Sunday, August 13 -------------------------------------------------------------
----------------------------------------------------------------------------------

09:00 - 10:00 Invited Talk

  Karem Sakallah.
  From Propositional Satisfiability to Satisfiability Modulo Theories.

10:00 - 10:30 Coffee

10:30 - 12:30 SMT

  Yinlei Yu and Sharad Malik.
  On Learning in SMT.

  Robert Nieuwenhuis and Albert Oliveras.
  On SAT Modulo Theories and Optimization Problems.

  Scott Cotton and Oded Maler.
  Fast and Flexible Difference Constraint Propagation for DPLL(T).

  Hossein Sheini and Karem Sakallah.
  A Progressive Simplifier for Satisfiability Modulo Theories.

12:30 - 14:00 Lunch

14:00 - 15:30 Structure

  Uwe Bubeck and Hans Kleine Büning.
  Dependency Quantified Horn Formulas: Models and Complexity.

  Stefan Porschen, Ewald Speckenmeyer and Bert Randerath.
  On Linear CNF Formulas.

  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 Coffee

16:00 - 18:00 Poster Session

19:00 - 22:00 Banquet

----------------------------------------------------------------------------------
-- Monday, August 14 -------------------------------------------------------------
----------------------------------------------------------------------------------

09:00 - 10:00 Invited Talk

  Fahiem Bacchus.
  CSPs: Adding Structure to SAT.

10:00 - 10:30 Coffee

10:30 - 12:30 QBF

  Hans Kleine Büning and Xishun Zhao.
  Minimal False Quantified Boolean Formulas.

  Horst Samulowitz and Fahiem Bacchus.
  Binary Clause Reasoning in QBF.

  Daijue Tang and Sharad Malik.
  Solving Quantified Boolean Formulas with Circuit Observability Don't Cares.

  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

14:00 - 16:00 MAX-SAT

  María Luisa Bonet, Jordi Levy and Felip Manyà.
  A Complete Calculus for Max-SAT.

  Zhaohui Fu and Sharad Malik.
  On Solving The Partial MAX-SAT Problem.

  Evgeny Dantsin and Alexander Wolpert.
  MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster than in O(2^n) Time.

* Osamu Watanabe and Masaki Yamamoto.
  Average-case analysis of the MAX-2SAT problem.

  Chu Min Li.
* MAX-SAT Evaluation.

16:00 - 16:30 Coffee

16:30 - 18:00 Kurt Gödel Keynote Session

  John Dawson.
  Shaken Foundations or Groundbreaking Realignment?
  A Centennial Assessment of Kurt Gödel's Impact on Logic, Mathematics, and Computer Science.

  Dana Scott.
  The Future of Proof.

----------------------------------------------------------------------------------
-- Tuesday, August 15 ------------------------------------------------------------
----------------------------------------------------------------------------------

09:00 - 10:00 Competition Session

  Olivier Roussel.
* Pseudo Boolean Evaluation.

  Armando Tacchella.
* QBF Evaluation.

  Carsten Sinz.
* SAT-Race.

10:00 - 10:30 Coffee

10:30 - 12:30 Local Search and Survey Propagation

  Steven Prestwich and Ines Lynce.
  Local Search for Unsatisfiability.

  Andrei Bulatov and Evgeny Skvortsov.
  Efficiency of Local Search.

  Panagiotis Manolios and Yimin Zhang.
  Implementing Survey Propagation Algorithm on Graphics Processing Units.

  Eric Hsu and Sheila McIlraith.
  Characterizing Propagation Methods for Boolean Satisfiability.

12:30 - 14:00 Lunch

14:00 - 15:30 Counting and Concurrency

  Naomi Nishimura, Prabhakar Ragde and Stefan Szeider.
  Solving #SAT using Vertex Covers.

  António Morgado, Paulo Matos, Vasco Manquinho and Joao Marques-Silva.
  Counting Models in Integer Domains.

* Marc Thurley.
  sharpSAT - counting models with advanced component caching and implicit BCP.

* Antti Eero Johannes Hyvärinen, Tommi Junttila and Ilkka Niemelä.
  A Distribution Method for Solving SAT in Grids.

15:30 - 16:00 Coffee

16:00 - 18:00 Poster Session

----------------------------------------------------------------------------------
[regular talks 30 minutes, short talks (marked '*') 15 minutes, incl. discussion]