SAT 2005 Technical Programme Eighth International Conference on Theory and Applications of Satisfiability Testing

June 19th-23rd 2005 University of St. Andrews Conference Centre St. Andrews, Scotland

The following papers will be presented during the conference's paper sessions.

• Solving Over-Constrained Problems with SAT Technology
  Josep Argelich and Felip Manya

• A Symbolic Search Based Approach for Quantified Boolean Formulas
  Gilles Audemard and Lakhdar Sais

• Substitutional Definition of Satisfiability in Classical Propositional Logic
  Anton Belov and Zbiginiew Stachniak

• A Clause-Based Heuristic for {SAT Solvers
  Nachum Dershowitz, Ziyad Hanna and Alexander Nadel

• Effective Preprocessing in {SAT through Variable and Clause Elimination
  Niklas Een and Armin Biere

• Resolution and Pebbling Games
  Nicola Galesi and Neil Thapen

• Local and Global Complete Solution Learning Methods for QBF
  Ian P. Gent and Andrew G.D. Rowley

• Equivalence checking of circuits with parameterized specifications
  Euguene Goldberg

• Observed Lower Bounds for Random 3-SAT Phase Transition Density using Linear Programming
  Marijn Heule and Hans van Maaren

• Simulating Cutting Plane proofs with restricted degree of falsity by Resolution
  Edward A. Hirsch and Sergey I. Nikolenko

• Resolution Tunnels for Improved SAT Performance
  Michal Kouril and John Franco

• Diversification and determinism in local search for satisfiability
  Chu Min Li and Wen Qi Huang

• On Finding All Minimally Unsatisfiable Subformulas
  Mark Liffiton and Karem Sakallah

• Optimizations for Compiling Declarative Models into Boolean Formulas
  Darko Marinov, Sarfraz Khurshid, Suhabe Bugrara, Lintao Zhang and Martin Rinard

• Random Walk With Continuously Smoothed Variable Weights
  Steven Prestwich

• Derandomization of PPSZ for Unique-k-SAT
  Daniel Rolf

• Heuristics for Fast Exact Model Counting
  Tian Sang and Paul Beame and Henry Kautz

• A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic
  Hossein M Sheini and Karem A. Sakallah

• DPvis - A Tool to Visualize the Structure of SAT Instances
  Carsten Sinz and Edda-Maria Dieringer

• Constraint Metrics for Local Search
  Finnegan Southey

• Input Distance and Lower Bounds for Propositional Resolution Proof Length
  Allen Van Gelder

• Sums of Squares, Satisfiability and Maximum Satisfiability
  Hans van Maaren and Linda van Norden

• Faster Exact Solving of SAT Formulae with a Low Number of Occurrences per Variables
  Magnus Wahlstrom

• A New Approach to Model Counting
  Wei Wei and Bart Selman

• Benchmarking SAT Solvers for Bounded Model Checking
  Emmnauel Zarpas

• On Subsumption Removal and On-the-Fly CNF Simplification
  Lintao Zhang

• Model-Equivalent Reductions
  Xishun Zhao and Hans Kleine Buning

The following papers will be presented during the conference's poster session.

• Improved Exact Solvers for Weighted Max-SAT
  Teresa Alsinet, Felip Manya and Jordi Planes

• Quantifier Trees for QBF
  Marco Benedetti

• Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas
  Uwe Bubeck, Hans Kleine Buning and Xishun Zhao

• A Branching Heuristic Directed for Quantified Renamable Horn Formulas
  Sylvie Coste-Marquis, Daniel Le Berre and Florian Letombe

• An Improved Upper Bound for SAT
  Evgeny Dantsin and Alexander Wolpert

• Bounded Model Checking with QBF
  Nachum Dershowitz, Ziyad Hanna and Jacob Katz

• Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies
  Vijay Durairaj and Priyank Kalla

• Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas
  Roman Gershman and Ofer Strichman

• Automatic Generation of Simplification Rules for SAT and MAXSAT
  Alexander S. Kulikov

• Speedup Techniques Utilized in Modern SAT Solvers
  Matthew T. Lewis, Tobias Schubert and Bernd W. Becker

• FPGA Logic Synthesis using Quantified Boolean Satisfiability
  Andrew C. Ling, Deshanand P. Singh and Stephen D. Brown

• On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization
  Vasco M. Manquinho and Joao Marques-Silva

• A New Set of Algebraic Benchmark Problems for SAT Solvers
  Andreas Meier and Volker Sorge

• A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas
  Maher N. Mneimneh, Ines Lynce, Zaher S. Andraus, Joao Marques-Silva, Karem A. Sakallah

• Threshold Behaviour of WalkSAT and Focused Metropolis Search on Random 3-Satisfiability
  Sakari Seitz, Mikko Alava and Pekka Orponen