SUNDAY, MAY 4TH

18:00-19:30

Registration Desk

 

MONDAY, MAY 5 TH

8:00-8:55

Registration Desk

 

8:55-9:20

Hans Kleine Büning, Zhao Xishun

Read-Once Unit Resolution

9:20-9:55

Stefan Porschen, Bert Randerath, Ewald Speckenmeyer

Linear Time Algorithms for some Not-all-Equal Satisfiability Problems

9:55-10:20

Nadia Creignou, Hervé Daudé

Crossed classification, complexity versus phase transition, for Boolean CSPs

10:20-10:50

Coffee Break

 

10:50-11:15

Hubie Chen

An Algorithm for SAT Above the Threshold

11:15-11:40

Ryan Williams

On Computing k-CNF Formula Properties

11:40-12:05

Sven Baumer, Rainer Schuler

Improving a probabilistic 3-SAT Algorithm by Dynamic Search and Independent Clause Pairs

12:05-12:30

Oliver Kullmann

On some connections between linear algebra and the combinatorics of clause-sets

12:30-14:00

Lunch

 

14:00- 15:00

Invited speaker: Riccardo Zecchina

Survey Propagation: from analytic results on random k-sat to a

message-passing algorithm for satisfiability

15:00-15:25

Giorgio Parisi

On the probabilistic approach to the random satisfiability problem

15:25-15:50

Guilhem Semerjian, Remi Monasson

A study of Pure Random Walk on Random Satisfiability Problems with physical methods

15:50-16:15

Hans van Maaren, Linda van Norden

Hidden threshold phenomena for fixed-density SAT-formulae

16:15-16:45

Coffee Break

 

16:45-17:10

Stefan Szeider

On fixed-parameter tractable parameterizations of SAT

17:10-17:35

Daniele Pretolani

Satisfiability Problems in Partial 2-hypertrees

17:35-18:00

Youichi Hanatani, Takashi Horiyama, Kazuo Iwama

Density Condensation of Boolean Formulas

18:00-18:25

Eugene Goldberg, Yakov Novikov

How good are current resolution based SAT-solvers?

19.30

Welcome Reception

 

 

TUESDAY, MAY 6 TH

8:30-9:30

Invited speaker: Toby Walsh

Challenges in SAT (and QBF)

9:30-9:55

J.Franco, M.Kouril, J.Schlipf, J.Ward, S.Weaver, M.Dransfield, W.M.Vanfleet

SBSAT: A State-Based, BDD-Based Satisfiability Solver

9:55-10:20

Ashish Sabharwal, Paul Beame, Henry Kautz

Using Problem Structure for Efficient Clause Learning

10:20-10:50

Coffee Break

 

10:50-11:15

Marc Herbstritt, Bernd Becker

Conflict-based Selection of Branching Rules

11:15-11:40

Lyndon Drake, Alan Frisch

The Interaction Between Inference and Branching Heuristics

11:40-12:05

Fahiem Bacchus, Jonathan Winter

Effective Preprocessing with Hyper-Resolution and Equality Reduction

12:05-12:30

Lintao Zhang, Sharad Malik

Cache Performance of SAT Solvers: A Case Study for Efficient Implementation of Algorithms

12:30-12:55

Paolo Liberatore

Algorithms and Experiments on Finding Minimal Models

12:55-14:25

Lunch

 

14:25-14:50

Enrico Giunchiglia, Marco Maratea, Armando Tacchella

Look-Ahead vs. Look-Back Techniques in a Modern SAT Solver

14:50-15:15

Ryan Williams, Carla Gomes, Bart Selman

On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search

15:15-15:40

Yannet Interian

Backdoor sets for random 3-SAT

15:40-16:05

Lintao Zhang, Sharad Malik

Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formula

16:05-16:35

Per Bjesse, James Kukula, Robert Damiano, Ted Stanion, Yunshan Zhu

Guiding SAT Diagnosis with Tree Decompositions

16:35-

Poster Session

 

WEDNESDAY, MAY 7 TH

8:30-8:55

Franc Brglez, Matthias F. Stallmann, Xiao Yu Li

SATbed: An Environment For Reliable Performance Experiments with SAT Instance Classes and Algorithms

8:55-12:30

Solvers presentation and Competition/Evaluation results:

 

1) Presentation of SAT solvers participating to the competition

 

2) Presentation of the results + awards

 

3) Presentation of the QBF solvers participating the evaluation

 

4) Presentation of the results

 

5) Discussion about the next SAT/QBF competitions

12:30-14:00

Lunch

 

 

THURSDAY, MAY 8 TH

8:30-9:30

Invited speaker: Wolfgang Kunz

ATPG versus SAT: comparing two paradigms for Boolean reasoning

9:30-9:55

Scott Diehl, Kevin Compton

An implementation of the polynomial calculus as a SAT solver

9:55-10:20

Renato Bruni

Solving Error Correction for Large Data Sets as Propositional Satisfiability

10:20-10:50

Coffee Break

 

10:50-11:15

Alessandro Armando, Luca Compagna

Automatic Analysis of Security Protocols via Reduction to SAT

11:15-11:40

Elizabeth Broering, Satyanarayana V. Lokam

Width-based Algorithms for SAT and CIRCUIT-SAT

11:40-12:05

Edmund Clarke, Muralidhar Talupur, Dong Wang

SAT based Predicate Abstraction for Hardware Verification

12:05-12:30

Sarfraz Khurshid, Darko Marinov, Ilya Shlyakhter, Daniel Jackson

A Case for Efficient Solution Enumeration

12:30-14:00

Lunch

 

14:00-14:25

Michael R. Dransfield, Victor W. Marek, Miroslaw Truszczynski

Satisfiability and Computing van der Waerden numbers

14:25-14:50

Hans Kleine Büning, K. Subramani, Xishun Zhao

On Boolean Models for Quantified Boolean Horn Formulas

14:50-15:15

Ian Gent, Enrico Giunchiglia, Massimo Narizzano, Andrew Rowley, Armando Tacchella

Watched Data Structures for QBF Solvers

15:15-15:40

Maher Mneimneh, Karem Sakallah

Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution

15:40-16:05

U. Egly, M. Seidl, H. Tompits, S. Woltran, M. Zolda

Comparing Different Prenexing Strategies for Quantified Boolean Formulas

16:05-16:35

Coffee Break

 

16:35-17:00

Xiao Yu Li, Matthias F. Stallmann, Franc Brglez

QingTing: A Fast SAT Solver Using Local Search and Efficient Unit Propagation

17:00-17:25

Steven Prestwich

Local Search on SAT-Encoded CSPs

17:25-17:50

Christian Bessiere, Emmanuel Hebrard, Toby Walsh

Local Consistencies in SAT

17:50-18:15

Teresa Alsinet, Felip Manya, Jordi Planes

Improved Branch and Bound Algorithms for Max-SAT

     

 

POSTER PRESENTATIONS:

 

Calin Anton, Joseph Culberson

Generating Instances of Intermediate Hardness for Satisfiability

Hui Xu, Rob A. Rutenbar

Insights from Almost Satisfied: Quantifying the Fine-Structure of Unsatisfiability for 3-SAT Phase T

Eduardo Rodriguez-Tello, Jose Torres-Jimenez

SAT Solving Using a GA and an Epistasis Reducer Algorithm.

Roland Yap, Stella Wang, Martin Henz

Real-time Reconfigurable Hardware WSAT Variants

M. Baioletti, A. Capotorti, S. Tulipani

Procedures for the CPA problem based on the elimination of Boolean constraints

Shlomit Bergman, Eliezer L. Lozinskii

A Fast Algorithm for MAX-SAT Approximation

James M. McQuillan, Craig A. Damon

Random versus non-random 3-CNF expressions, 3-SAT, and Davis-Putnam

Martin Fürer

Forced Horn Satisfiability

Ilya Shlyakhter, Manu Sridharan, Robert Seater, Daniel Jackson

Exploiting Subformula Sharing in Automatic Analysis of Quantified Formulas

Inês Lynce, João Marques-Silva

On Implementing More Efficient SAT Data Structures

Yimin Zhang, Hai Lin, JiGui Sun, DanTong Ou Yang

Generating SAT Instances Using One-way Hash Function

Zbigniew Lonc, Miroslaw Truszczynski

Computing all models of CNF theories

Sarah Ibri, Habiba Drias

Parallel ACS for weighted MAX-SAT

Gilles Audemard, Daniel Le Berre, Olivier Roussel, Inês Lynce, João Marques-Silva

OpenSAT: An Open Source SAT Software Project