SAT 2005

Eighth International Conference on
Theory and Applications of Satisfiability Testing

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

Sunday June 19th

17.00-18.00 Registration.
18.15-18.45 Dinner.
19.00-20.00 Registration.
19.00-Late. Scottish pub.

Monday June 20th

08.00-08.45  Breakfast.
08.30-09.15 Registration.
09.15-10.30 Paper Session ISAT solving
Chair: Joao Marques Silva.

Effective Preprocessing in SAT through Variable and Clause Elimination.

Niklas Een and Armin Biere.

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

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

10:40-11:15 Coffee break.
11:15-12:30 Paper Session IILocal search
Chair: Hans van Maaren.

Constraint Metrics for Local Search.
Finnegan Southey.

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

Random Walk With Continuously Smoothed Variable Weights.
Steven Prestwich.

12:30-14:00 Lunch.
14:00-15:00 Invited talkSAT in Formal Hardware Verification.
Armin Biere.
15:00-15:30 Poster Session IIntroductions.

Coffee Served at 15:30

Poster Session II

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.

19:00-19:45 Conference Reception, Lower College Hall.
19:45-Late Conference Dinner, Lower College Hall.

Tuesday June 21st

08.00-08.45 Breakfast.
09:00-10:40 Paper Session IIIExtensions.
Chair: Hans Kleine Buning

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

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

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

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

10:40-11:15 Coffee.
11:15-12:30 Paper Session IVSpecialized methods.
Chair: Ian Gent

Equivalence checking of circuits with parameterized specifications.
Euguene Goldberg.

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

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

12:30-12:40 Preview of SAT 2006
12:40-14:00 Lunch.
14:00-15:00 Presentation of Competition Results.
15:00-15:30 Poster Session IIIntroductions.

Coffee Served at 15:30

Poster session II

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.

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

18:30 Dinner
20:00-Late Whisky Tasting.

Wednesday June 22nd

08.00-08.45 Breakfast.
09:00-10:40 Paper Session VProof complexity.
Chair: Paul Beame

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

Resolution and Pebbling Games.
Nicola Galesi and Neil Thapen.

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

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

10:40-11:10 Coffee.
11:10-12:00 Paper Session VIQBF and Max Sat
Chair: Armin Biere

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

Model-Equivalent Reductions.
Xishun Zhao and Hans Kleine Buning.

12:00-13:30 Lunch.
13:30-18.00 Excursion to Falkland Palace.
18:30 Dinner

Thursday June 23rd

08.00-08.45 Breakfast.
09:00-10:40 Paper Session VIIRandom problems and benchmarking.
Chair: Holger Hoos

Benchmarking SAT Solvers for Bounded Model Checking.
Emmnauel Zarpas.

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

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

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

10:40-11:15 Coffee.
11:15-12:30 Paper Session VIIISAT and QBF theory.
Chair: John Franco

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

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

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

12:30-14:00 Lunch
14:00-15:00 Invited talkSatisfiability and Unsatisfiability.
Paul Beame
15:00-15:30 Coffee
15:30 Conference ends.