%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 %I endm9002 %D panel3 %T Generating effective symmetry-breaking predicates for search problems %N Ilya Shlyakhter %E ilya_shl@mit.edu %I endm9003 %D long %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 %D long %T Satisfiability Formulas Closed Under Replacements %N Hans Kleine Büning %C Zhao Xishun %E kbcsl@uni-paderborn.de %I endm9005 %D poster %T Introduction to QSpace %N Dan Pehoushek %E danpehous@yahoo.com %I endm9006 %D panel4 %T Exploiting the real power of unit propagation lookahead %N Daniel Le Berre %E daniel@cafe.newcastle.edu.au %I endm9007 %D long %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 %D long %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 %D long %T Proving unsatisfiability of CNFs locally %N Eugene Goldberg %E egold@cadence.com %I endm90010 %D long %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 %D panel4 %T Combining Preorder and Postorder Resolution in a Satisfiability Solver %N Allen Van Gelder %E avg@cs.ucsc.edu %I endm9012 %D long %T SatEx: A Web-based Framework for SAT Experimentation %N Laurent Simon %E simon@lri.fr %C Philippe Chatalic %I endm9013 %D poster %T Criticality and Parallelism in GSAT %N Andrea Roli %E aroli@deis.unibo.it, aroli@ulb.ac.be %I endm9014 %D panel2 %T Restoring Satisfiability or Maintaining Unsatisfiability by finding small Unsatisfiable Subformulae %N Renato Bruni %E bruni@dis.uniroma1.it %C Antonio Sassano %I endm9015 %D short %T Parallelizing Satz Using Dynamic Workload Balancing %N B. Jurkowiak %E jurkowia@laria.u-picardie.fr %C Chu Min Li, Gil Utard %I endm9016 %D panel2 %T Stochastic Systematic Search Algorithms for Satisfiability %N I. Lynce %C L. Baptista, J. Marques-Silva, jpms@inesc.pt %I endm9017 %D long %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 %D panel2 %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 %D panel4 %T Autarkies for satisfiability decision %N Oliver Kullmann %E kullmann@cs.toronto.edu %I endm9020 %D long %T The Unreasonable Effectiveness of Alternation Centered Satisfiabilty Algorithms %N Tom Morrisette %E thomas.morrisette@db.com %I endm9021 %D poster %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 %D panel3 %T Exploiting Partial Knowledge of Satisfying Assignments %N Kazuo Iwama %E iwama@kuis.kyoto-u.ac.jp %C Suguru Tamaki %I endm9023 %D short %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 %D panel1 %T Towards an efficient library for SAT %N Armando Tacchella %E tac@cs.rice.edu %C Enrico Giunchiglia, Moshe Vardi %I endm9025 %D poster %T Theorem Proving with Structured Theories %N Sheila McIlraith %E sam@ksl.stanford.edu %C Eyal Amir %I endm9026 %D short %T Partition-Based Satisfiability and the Most Constrained Subproblem %N Eyal Amir %E eyal@cs.stanford.edu %C Sheila McIlraith %I endm9027 %D poster %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 %D panel1 %T Self-Tuning Walksat %N Don Patterson %E djp3@cs.washington.edu %I endm9029 %D panel1 %T A polyhedral projection procedure for Q2SAT %N K Subramani %E ksmani@csee.wvu.edu %I endm9030 %D poster %T A Bayesian Approach to Tackling Hard Computational Problems %N Henry Kautz %E horvitz@MICROSOFT.com %C Eric Horvitz, Yongshao Ruan, Carla Gomes, Bart Selman, Max Chickering %I endm9031 %D panel1 %T Resolution versus analytic tableaux %N Alasdair Urquhart %E urquhart@cs.toronto.edu %I endm9032 %D invited talk %T SAT Problems Arising From Software Design Checking %N Daniel Jackson %E dnj@lcs.mit.edu %I endm9033 %D invited talk %T Stochastic Satisfiability: Algorithms and Applications %N Michael Littman %E mlittman@research.att.com %I endm9034 %D invited talk %P no paper %T To be announced %N H. van Maaren %E h.vanmaaren@its.tudelft.nl %I endm9035 %D poster %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 %D panel4 %T Conflict-directed A* and Its Role in Model-based Embedded Systems %N Brian Williams %E williams@mit.edu %I endm9037 %D panel3