8. SAT 2005: St. Andrews, UK

• Josep Argelich, Felip Manyà:
  Solving Over-Constrained Problems with SAT Technology. 1-15
  
• Gilles Audemard, Lakhdar Sais:
  A Symbolic Search Based Approach for Quantified Boolean Formulas. 16-30
  
• Anton Belov, Zbigniew Stachniak:
  Substitutional Definition of Satisfiability in Classical Propositional Logic. 31-45
  
• Nachum Dershowitz, Ziyad Hanna, Alexander Nadel:
  A Clause-Based Heuristic for SAT Solvers. 46-60
  
• Niklas Eén, Armin Biere:
  Effective Preprocessing in SAT Through Variable and Clause Elimination. 61-75
  
• Nicola Galesi, Neil Thapen:
  Resolution and Pebbling Games. 76-90
  
• Ian P. Gent, Andrew G. D. Rowley:
  Local and Global Complete Solution Learning Methods for QBF. 91-106
  
• Eugene Goldberg:
  Equivalence Checking of Circuits with Parameterized Specifications. 107-121
  
• Marijn Heule, Hans van Maaren:
  Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming. 122-134
  
• Edward A. Hirsch, Sergey I. Nikolenko:
  Simulating Cutting Plane Proofs with Restricted Degree of Falsity by Resolution. 135-142
  
• Michal Kouril, John V. Franco:
  Resolution Tunnels for Improved SAT Solver Performance. 143-157
  
• Chu Min Li, Wen Qi Huang:
  Diversification and Determinism in Local Search for Satisfiability. 158-172
  
• Mark H. Liffiton, Karem A. Sakallah:
  On Finding All Minimally Unsatisfiable Subformulas. 173-186
  
• Darko Marinov, Sarfraz Khurshid, Suhabe Bugrara, Lintao Zhang, Martin C. Rinard:
  Optimizations for Compiling Declarative Models into Boolean Formulas. 187-202
  
• Steven David Prestwich:
  Random Walk with Continuously Smoothed Variable Weights. 203-215
  
• Daniel Rolf:
  Derandomization of PPSZ for Unique- k-SAT. 216-225
  
• Tian Sang, Paul Beame, Henry A. Kautz:
  Heuristics for Fast Exact Model Counting. 226-240
  
• Hossein M. Sheini, Karem A. Sakallah:
  A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic. 241-256
  
• Carsten Sinz, Edda-Maria Dieringer:
  DPvis - A Tool to Visualize the Structure of SAT Instances. 257-268
  
• Finnegan Southey:
  Constraint Metrics for Local Search. 269-281
  
• Allen Van Gelder:
  Input Distance and Lower Bounds for Propositional Resolution Proof Length. 282-293
  
• Hans van Maaren, Linda van Norden:
  Sums of Squares, Satisfiability and Maximum Satisfiability. 294-308
  
• Magnus Wahlström:
  Faster Exact Solving of SAT Formulae with a Low Number of Occurrences per Variable. 309-323
  
• Wei Wei, Bart Selman:
  A New Approach to Model Counting. 324-339
  
• Emmanuel Zarpas:
  Benchmarking SAT Solvers for Bounded Model Checking. 340-354
  
• Xishun Zhao, Hans Kleine Büning:
  Model-Equivalent Reductions. 355-370
  
• Teresa Alsinet, Felip Manyà, Jordi Planes:
  Improved Exact Solvers for Weighted Max-SAT. 371-377
  
• Marco Benedetti:
  Quantifier Trees for QBFs. 378-385
  
• Uwe Bubeck, Hans Kleine Büning, Xishun Zhao:
  Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas. 386-392
  
• Sylvie Coste-Marquis, Daniel Le Berre, Florian Letombe:
  A Branching Heuristics for Quantified Renamable Horn Formulas. 393-399
  
• Evgeny Dantsin, Alexander Wolpert:
  An Improved Upper Bound for SAT. 400-407
  
• Nachum Dershowitz, Ziyad Hanna, Jacob Katz:
  Bounded Model Checking with QBF. 408-414
  
• Vijay Durairaj, Priyank Kalla:
  Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies. 415-422
  
• Roman Gershman, Ofer Strichman:
  Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas. 423-429
  
• Alexander S. Kulikov:
  Automated Generation of Simplification Rules for SAT and MAXSAT. 430-436
  
• Matthew D. T. Lewis, Tobias Schubert, Bernd Becker:
  Speedup Techniques Utilized in Modern SAT Solvers. 437-443
  
• Andrew C. Ling, Deshanand P. Singh, Stephen Dean Brown:
  FPGA Logic Synthesis Using Quantified Boolean Satisfiability. 444-450
  
• Vasco M. Manquinho, João P. Marques Silva:
  On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization. 451-458
  
• Andreas Meier, Volker Sorge:
  A New Set of Algebraic Benchmark Problems for SAT Solvers. 459-466
  
• Maher N. Mneimneh, Inês Lynce, Zaher S. Andraus, João P. Marques Silva, Karem A. Sakallah:
  A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas. 467-474
  
• Sakari Seitz, Mikko Alava, Pekka Orponen:
  Threshold Behaviour of WalkSAT and Focused Metropolis Search on Random 3-Satisfiability. 475-481
  
• Lintao Zhang:
  On Subsumption Removal and On-the-Fly CNF Simplification. 482-489