Conference Programme

Summary

 

 

July 11

July 12

July 13

July 14

09:00-10:00    

Invited - Naveh

Invited - Paturi

Plenary - Gottlob

Tutorial

10:00-10:30

Break

Break

Break

Break

10:30-12:30

Heuristics

Theory + Combinatorics

Random + Statistics/LS

Optimization + SAT Usage

12:30-14:00

Lunch Break

Lunch Break

Lunch Break

Lunch Break

14:00-15:00

Plenary - Harel

SAT Usage

Plenary - Moore

SMT

15:00-15:30

Break

Break

Break

Break

15:30-

Theory + Combinatorics

QBF

QBF

Competitions

 

 

 

Business Meeting

 

End time

17:30

17:20

18:00

17:30



And here is the same list with session chairs.

Schedule

 

Sunday, July 11

 

 

 

Session I: SAT Invited Talk

09:00-10:00

Yehuda Naveh. The Big Deal: Applying Constraint Satisfaction Technologies Where it Makes the Difference

10:00-10:30

Break

 

 

 

Session II: Heuristics

10:30-11:00

Stephan Kottler. SAT Solving with Reference Points

11:00-11:30

Dave Tompkins and Holger Hoos. Dynamic Scoring Functions with Variable Expressions: New SLS Methods for Solving SAT

11:30-11:50

Alexander Nadel and Vadim Ryvchin. Assignment Stack Shrinking

11:50-12:10

Matti Jarvisalo and Armin Biere. Reconstructing Solutions after Blocked Clause Elimination

12:10-12:30

Ashish Sabharwal, Bart Selman and Lukas Kroc. An Empirical Study of Optimal Noise and Runtime Distributions in Local Search

12:30-14:00

Lunch Break

 

 

 

Session III: FLoC Plenary

14:00-15:00

David Harel. Amir Pnueli: A Gentle Giant, Lord of the Phi's and the Psi's

15:00-15:30

Break

 

 

 

Session IV: Theory + Combinatorics

15:30-16:00

Masaki Yamamoto, Kazuhisa Makino and Suguru Tamaki. An Exact Algorithm for the Boolean Connectivity Problem for k-CNF

16:00-16:30

Hadi Katebi, Karem Sakallah and Igor Markov. Symmetry and Satisfiability: An Update

16:30-17:00

Stefan Porschen, Tatjana Schmidt and Ewald Speckenmeyer. Complexity Results for Linear XSAT Problems

17:00-17:30

Olaf Beyersdorff, Arne Meier, Sebastian Mueller, Michael Thomas and Heribert Vollmer. Proof Complexity of Propositional Default Logic

 

Monday, July 12

 

 

 

Session I: SAT Invited Talk

09:00-10:00

Ramamohan Paturi. Exact Algorithms and Complexity

10:00-10:30

Break

 

 

 

Session II: Theory + Combinatorics

10:30-11:00

Evgeny Dantsin and Alexander Wolpert. On Moderately Exponential Time for SAT

11:00-11:30

Eli Ben-Sasson and Jan Johannsen. Lower bounds for width-restricted clause learning on small width formulas

11:30-11:50

Scott Cotton. Some Techniques for Minimizing Resolution Proofs

11:50-12:10

Allen Van Gelder and Ivor Spence. Zero-One Designs Produce Small Hard SAT Instances

12:10-12:30

William Matthews and Ramamohan Paturi. Uniquely Satisfiable k-SAT Instances with Almost Minimal Occurrences of Each Variable

12:30-14:00

Lunch Break

 

 

 

Session III: SAT Usage

14:00-14:30

Carsten Fuhs and Peter Schneider-Kamp. Synthesizing Shortest Straight-Line Programs over GF(2) using SAT

14:30-14:50

Oliver Kullmann. Green-Tao Numbers and SAT

15:00-15:30

Break

 

 

 

Session IV: QBF

15:30-16:00

Uwe Bubeck and Hans Kleine Buning. Rewriting (Dependency-) Quantified 2-CNF with Arbitrary Free Literals into Existential 2-HORN

16:00-16:30

Christian Miller, Stefan Kupferschmid, Matthew Lewis and Bernd Becker. Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs

16:30-17:00

Enrico Giunchiglia, Paolo Marin and Massimo Narizzano. sQueezeBF: An effective preprocessor for QBFs

17:00-17:20

Alexandra Goultiaeva and Fahiem Bacchus. Exploiting Circuit Representations in QBF Solving

 

Tuesday, July 13

 

 

 

Session I: FLoC Plenary

09:00-10:00

Georg Gottlob. Datalog+-: A Family of Logical Query Languages for New Applications

10:00-10:30

Break

 

 

 

Session II: Random + Statistics/LS

10:30-11:00

Vishwambhar Rathi, Erik Aurell, Lars Rasmussen and Mikael Skoglund. Bounds on Threshold of Regular Random k-SAT

11:00-11:30

Thomas Hugel and Yacine Boufkhad. Non Uniform Selection of Solutions for Upper Bounding the 3-SAT Threshold

11:30-11:50

Mladen Nikolic. Statistical Methodology for Comparison of SAT Solvers

11:50-12:10

Adrian Balint and Andreas Frohlich. Improving stochastic local search for SAT with a new probability distribution

12:10-12:30

Anton Belov and Zbigniew Stachniak. Improved Local Search for Circuit Satisfiability

12:30-14:00

Lunch Break

 

 

 

Session III: FLoC Plenary

14:00-15:00

J Strother Moore. Theorem Proving for Verification: The Early Days

15:00-15:30

Break

 

 

 

Session IV: QBF

15:30-16:00

Robert Brummayer, Florian Lonsing and Armin Biere. Automated Testing and Debugging of SAT and QBF Solvers

16:00-16:30

William Klieber, Samir Sapra, Sicun Gao and Edmund Clarke. A Non-Prenex, Non-Clausal QBF Solver with Game-State Learning

16:30-17:00

Florian Lonsing and Armin Biere. Integrating Dependency Schemes in Search-Based QBF Solvers

 

 

17:00-18:00

SAT Business meeting

 

Wednesday, July 14

 

 

 

Session I: SAT Invited Tutorial

09:00-10:00

Daniel Kroening: A Primer on the Algorithmic Aspects of Satisfiability Modulo Theories

10:00-10:30

Break

 

 

 

Session II: Optimization + SAT Usage

10:30-11:00

Vasco Manquinho, Ruben Martins and Ines Lynce. Improving Unsatisfiability-based Algorithms for Boolean Optimization

11:00-11:30

Denis Pankratov and Allan Borodin. On the Relative Merits of Simple Local Search Methods for the Max Sat Problem

11:30-11:50

Chu-Min LI, Felip Manya, Zhe Quan and Zhu Zhu. Exact MinSAT Solving

11:50-12:10

Ruediger Ehlers. Minimizing Deterministic Buchi Automata Precisely using SAT Solving

12:10-12:30

Gayathri Namasivayam and Miroslaw Truszczynski. Simple but Hard Mixed Horn Formulas

12:30-14:00

Lunch Break

 

 

 

Session III: Joint SAT/SMT session

14:00-14:20

(SAT'10) Miquel Bofill, Josep Suy and Mateu Villaret. A system for solving constraint satisfaction problems with SMT

14:20-14:50

(SMT'10) J. Christ, J. Hoenicke. Instantiation-Based Interpolation for Quantified Formulae

15:00-15:30

Break

 

 

 

Session IV: Competitions

15:30-16:00

Claudia Peschiera, Luca Pulina, Armando Tacchella, Uwe Bubeck, Oliver Kullmann and Ines Lynce. The Seventh QBF Solvers Evaluation (QBFEVAL'10)

16:00-16:30

Results of the Max-SAT Evaluation. Presented by Josep Argelich.

16:30-17:00

Results of the SAT-Race. Presented by Carsten Sinz.

17:00-17:30

Results of the PB Evaluation. Presented by Daniel Le-Berre.

 

 

 

End