SAT 2004 - PRELIMINARY PROGRAMME (subject to minor changes) ------------------ Sunday, 9 May 2004 ------------------ 19:00-21:00 Reception (Renaissance Hotel) Food, drinks, good company - registration open ------------------- Monday, 10 May 2004 ------------------- 9:00-9:20 Opening 9:20-10:10 Session 1 [Hard instances] 1) A Random Constraint Satisfaction Problem That Seems Hard for DPLL Harold Connamacher 2) From spin glasses to hard satisfiable formulas Haixia Jia, Cris Moore and Bart Selman 10:50-12:30 Session 2 [SAT Solvers] 1) Combining Component Caching and Clause Learning for Effective Model Counting Tian Sang, Fahiem Bacchus, Paul Beame, Henry Kautz, Toniann Pitassi 2) Early Conflict Detection Based BCP for SAT Solving Matthew D. T. Lewis, Tobias Schubert, Bernd W. Becker 3) UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT and MAX-SAT Dave A. D. Tompkins and Holger H. Hoos 4) CirCUs: Hybrid Satifiability solver HoonSang Jin, Fabio Somenzi 14:20-15:20 Invited Talk Ken McMillan, Cadence Berkely Labs: (title TBA) 15:50-16:40 Session 3 [Algorithms and Bounds I] 1) Algorithms for Satisfiability using Independent Sets of Variables Ravi Gummadi, N.S. Narayanaswamy, Venkatakrishnan Ramaswamy 2) Approximation algorithm for random MAX-KSAT Yannet Interian 16:40-18:00 SAT Solvers Competition & QBF Solvers Evaluation Results & Discussion --------------- Tuesday, 11 May --------------- 9:00-10:15 Session 4 [Algorithms and Bounds II] 1) Derandomization of Schuler's Algorithm for SAT Evgeny Dantsin and Alexander Wolpert 2) Polynomial time SAT decision, hypergraph transversals and the Hermitian rank Nicola Galesi and Oliver Kullmann 3) Computing Unsatisfiable k-SAT Instances with Few Occurrences per Variable Shlomo Hoory, Stefan Szeider 10:50-12:30 Session 5 [Properties of Formulae / Non-Boolean Problems] 1) Detecting Backdoor Sets with Respect to Horn and Binary Clauses Naomi Nishimura, Prabhakar Ragde, and Stefan Szeider 2) A Note on Satisfying Truth-Value Assignments of Boolean Formulas Zbigniew Stachniak 3) Mapping problems with finite-domain variables into problems with Boolean variables Carlos Ansotegui and Felip Manya 4) Using Lower-Bound Estimates in SAT-Based Pseudo-Boolean Optimization Vasco M. Manquinho, Joao Marques-Silva 14:20-15:20 Poster overview session I Worst Case Bounds for some NP-Complete Modified Horn-SAT Problems Stefan Porschen, Ewald Speckenmeyer Satisfiability Threshold of the Skewed Random k-SAT (Poster / Short Paper) Danila A. Sinopalnikov Local Search for Very Large SAT Problems (Poster / Short Paper) Steven Prestwich and Colin Quirke Local search with bootstrapping (Poster / Short Paper) Lengning Liu and Miroslaw Truszczynski Efficient Implementations of SAT Local Search (Poster / Short Paper) Alex Fukunaga Adding a New Conflict Based Branching Heuristic in two Evolved DPLL SAT Solvers (Poster / Short Paper) Renato Bruni, Andrea Santori Using Rewarding Mechanisms for Improving Branching Heuristics (Poster / Short Paper) Elsa Carvalho & Joao Marques-Silva On Computing Minimum Unsatisfiable Cores (Poster / Short Paper) Ines Lynce and Joao P. Marques-Silva Visualizing the Internal Structure of SAT Instances (Preliminary Report) (Poster / Short Paper) Carsten Sinz 15:20-16:20 Poster session I + coffee 16:20-18:00 Session 6 [Non-CNF SAT I] 1) Using DPLL for Efficient OBDD Construction Jinbo Huang and Adnan Darwiche 2) Search vs. Symbolic Techniques in Satisfiability Solving Guoqiang Pan, Moshe Y. Vardi 3) Solving Non-Clausal Formulas with DPLL search Christian Thiffault, Fahiem Bacchus, Toby Walsh 4) Automatic extraction of functional dependencies Eric Gregoire, Richard Ostrowski, Bertrand Mazure and Lakhdar Sais ---------------------- Wednesday, 12 May 2004 ---------------------- 9:00-10:15 Invited talk Stephen Cook, University of Toronto: (title TBA) 10:50-12:30 Session 7 [Non-CNF SAT II] 1) A SAT-based Decision Procedure for the Boolean Combination of Difference Constraints Alessandro Armando and Claudio Castellini and Enrico Giunchiglia and Marco Maratea 2) Aligning CNF- and Equivalence-Reasoning Marijn Heule and Hans van Maaren 3) An algebraic approach to the complexity of generalized conjunctive queries Michael Bauland, Philippe Chapdelaine, Nadia Creignou, Miki Hermann, Heribert Vollmer 4) A SAT Based Scheduler for Fair Tournament Schedules Hantao Zhang, Dapeng Li, and Haiou Shen 14:00-0:30 Excursion + Banquet Details TBA --------------------- Thursday, 13 May 2004 --------------------- 9:00-10:15 Session 8 [Bounded Model Checking] 1) Encoding Global Unobservability for Efficient Translation to SAT Miroslav N. Velev 2) Incremental Compilation-to-SAT procedures Marco Benedetti and Sara Bernardini 3) Analysis of Search Based Algorithms for Satisfiability of Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems Daijue Tang, Yinlei Yu, Darsh P. Ranjan, Sharad Malik 10:50-12:30 Session 9 [QBF] 1) Looking Algebraically at Tractable Quantified Boolean Formulas Hubie Chen and Victor Dalmau 2) Equivalence Models for Quantified Boolean Formulas Hans Kleine Buening, Xishun Zhao 3) Resolve and Expand Armin Biere 4) QBF reasoning on real-world instances Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella 14:20-15:20 Poster overview session II A Comparative Study of 2QBF Algorithms (Poster / Short Paper) Darsh P. Ranjan, Daijue Tang, Sharad Malik Dealing with symmetries in Quantified Boolean Formulas (Poster / Short Paper) Gilles Audemard, Bertrand Mazure and Lakhdar Saïs Improving First-order Model Searching by Propositional Reasoning and Lemma Learning (Poster / Short Paper) Zhuo Huang, Hantao Zhang and Jian Zhang Boolean Ring Satisfiability (Poster / Short Paper) Nachum Dershowitz, Jieh Hsiang, Guan-Shieng Huang, and Daher Kaiss Game-SAT: A Preliminary Report (Poster / Short Paper) Ling Zhao and Martin Mueller Verifying the On-Line Help System of SIEMENS Magnetic Resonance Tomographs using SAT (Poster / Short Paper) Carsten Sinz and Wolfgang Kuchlin NiVER: Non Increasing Variable Elimination Resolution for Preprocessing SAT instances (Poster / Short Paper) Sathiamoorthy Subbarayan and Dhiraj K Pradhan The Optimality of a Fast CNF Conversion and its use with SAT (Poster / Short Paper) Daniel Sheridan Problem encoding into SAT : the counting constraints case (Poster / Short Paper) Olivier Bailleux and Yacine Boufkhad 15:20-16:20 Poster session II [end of conference]