Schedule LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT2001) (Revised Tue May 15 16:37:44 PDT 2001) -------------------------------------------------------------------------------------- Thursday June 14 9:00 %T SAT Problems Arising From Software Design Checking %N Daniel Jackson %E dnj@lcs.mit.edu %I endm9033 9:45 %T Stochastic Systematic Search Algorithms for Satisfiability %N I. Lynce %C L. Baptista, J. Marques-Silva %E jpms@inesc.pt %I endm9017 10:15 Coffee 10:30 %T Exploiting the real power of unit propagation lookahead %N Daniel Le Berre %E daniel@cafe.newcastle.edu.au %I endm9007 11:00 Panel: SAT Encodings of NP-Hard Problems %T Balance and Filtering in Structured Satisfiable Problems %N Henry Kautz %E gomes@cs.cornell.edu %C Yongshao Ruan, Dimitris Achlioptas, Carla Gomes, Bart Selman, Mark Stickel %I endm9002 %T A Satisfiability Formulation of Problems on Level Graphs %N Bert Randerath %E randerath@informatik.Uni-Koeln.DE %C Endre Boros, Ondrej Cepek, Peter Hammer, Alex Kogan, Kazuhisa Makino, Bruno Simeone, Ewald Speckenmeyer %I endm9022 11:30 %T Generating effective symmetry-breaking predicates for search problems %N Ilya Shlyakhter %E ilya_shl@mit.edu %I endm9003 12:00 Lunch 1:30 %T Conflict-directed A* and Its Role in Model-based Embedded Systems %N Brian Williams %E williams@mit.edu %I endm9037 2:00 Panel: Machine Learning %T Self-Tuning Walksat %N Don Patterson %E djp3@cs.washington.edu %I endm9029 %T Ensemble-based prediction of SAT search behaviour %N Breanndán Ó Nualláin %E bon@illc.uva.nl %C Maarten de Rijke, Johan van Benthem %I endm9024 %T A Bayesian Approach to Tackling Hard Computational Problems %N Eric Horvitz %E horvitz@MICROSOFT.com %C Yongshao Ruan, Henry Kautz, Carla Gomes, Bart Selman, Max Chickering %I endm9031 %T Learning to Select Branching Rules in the DPLL procedure for Satisfiability %N Michail G. Lagoudakis %E mgl@cs.duke.edu %C Michael L. Littman %I endm9028 3:00 Coffee 3:15 %T Autarkies for satisfiability decision %N Oliver Kullmann %E kullmann@cs.toronto.edu %I endm9020 3:45 %T Restoring Satisfiability or Maintaining Unsatisfiability by finding small Unsatisfiable Subformulae %N Renato Bruni %E bruni@dis.uniroma1.it %C Antonio Sassano %I endm9015 4:05 %T Exploiting Partial Knowledge of Satisfying Assignments %N Kazuo Iwama %E iwama@kuis.kyoto-u.ac.jp %C Suguru Tamaki %I endm9023 4:25 %T Theorem Proving with Structured Theories %N Sheila McIlraith %E sam@ksl.stanford.edu %C Eyal Amir %I endm9026 4:45 %T Engineering a (Super?) Efficient SAT Solver %N Matthew W. Moskewicz %C Conor Madigan, Ying Zhao, Lintao Zhang, Sharad Malik %E moskewcz@alumni.princeton.edu %I endm9009 5:15 End of Day -------------------------------------------------------------------------------------- Friday June 15 9:00 %T Stochastic Satisfiability: Algorithms and Applications %N Michael Littman %E mlittman@research.att.com %I endm9034 9:45 Panel: Beyond SAT %T Introduction to QSpace %N Dan Pehoushek %E danpehous@yahoo.com %I endm9006 %T Complexity and Approximability of Quantified and Stochastic Constraint Satisfaction Problems %N Madhav V. Marathe %E marathe@lanl.gov %C Harry B. Hunt III, Richard E. Stearns %I endm9019 10:15 Coffee 10:30 Panel Continued: Beyond SAT %T Phase Transitions of PP-Complete Satisfiability Problems %N Phokion G. Kolaitis %C Delbert D. Bailey, Victor Dalmau %E kolaitis@cse.ucsc.edu %I endm9011 %T Extending the Reach of SAT with Many-valued Logics %N Ramon Bejar %E bejar@cs.cornell.edu %C Alba Cabiscol, Cesar Fernandez, Felip Manya, and Carla Gomes %I endm9036 11:00 Poster Overviews 11:15 Poster Session 12:15 Lunch 1:30 %T Resolution versus analytic tableaux %N Alasdair Urquhart %E urquhart@cs.toronto.edu %I endm9032 2:15 %T Combining Preorder and Postorder Resolution in a Satisfiability Solver %N Allen Van Gelder %E avg@cs.ucsc.edu %I endm9012 2:45 Coffee 3:00 %T Proving unsatisfiability of CNFs locally %N Eugene Goldberg %E egold@cadence.com %I endm90010 3:30 %T Statistical physics analysis of the backtrack resolution of random 3-SAT instances. %N Remi Monasson %C Simona Cocco %E monasson@uchicago.edu %I endm9004 4:00 %T The unsatisfiability threshold revisited %N Alexis C. Kaporis %C Lefteris M. Kirousis, Yannis C. Stamatiou, Malvina Vamvakari, Michele Zito %E michele@csc.liv.ac.uk %I endm9008 4:30 Panel: Parallelism %T Criticality and Parallelism in GSAT %N Andrea Roli %E aroli@deis.unibo.it, aroli@ulb.ac.be %I endm9014 %T Parallelizing Satz Using Dynamic Workload Balancing %N B. Jurkowiak %E jurkowia@laria.u-picardie.fr %C Chu Min Li, Gil Utard %I endm9016 %T PaSAT - Parallel SAT-Checking with Lemma Exchange: %N Carsten Sinz %E sinz@informatik.uni-tuebingen.de %C Wolfgang Blochinger, Wolfgang Küchlin %I endm9018 5:15 End of Day -------------------------------------------------------------------------------------- Posters %T Satisfiability Formulas Closed Under Replacements %N Hans Kleine Büning %C Zhao Xishun %E kbcsl@uni-paderborn.de %I endm9005 %T SatEx: A Web-based Framework for SAT Experimentation %N Laurent Simon %E simon@lri.fr %C Philippe Chatalic %I endm9013 %T The Unreasonable Effectiveness of Alternation Centered Satisfiabilty Algorithms %N Tom Morrisette %E thomas.morrisette@db.com %I endm9021 %T Towards an efficient library for SAT %N Armando Tacchella %E tac@cs.rice.edu %C Enrico Giunchiglia, Moshe Vardi %I endm9025 %T Partition-Based Satisfiability and the Most Constrained Subproblem %N Eyal Amir %E eyal@cs.stanford.edu %C Sheila McIlraith %I endm9027 %T A polyhedral projection procedure for Q2SAT %N K Subramani %E ksmani@csee.wvu.edu %I endm9030 %T To be announced %N H. van Maaren %E h.vanmaaren@its.tudelft.nl %I endm9035 --------------------------------------------------------------------------------------