Program of SAT

Sunday, July 11th

Sunday's program is also available with abstracts and side by side with other events.

09:00‑10:00 SAT Invited Talk
Location: AT LT2
09:00 Yehuda Naveh
The Big Deal: Applying Constraint Satisfaction Technologies Where it Makes the Difference
10:30‑12:30 Heuristics
Location: AT LT2
10:30 Stephan Kottler
SAT Solving with Reference Points
11:00 Dave Tompkins and Holger Hoos
Dynamic Scoring Functions with Variable Expressions: New SLS Methods for Solving SAT
11:30 Alexander Nadel and Vadim Ryvchin
Assignment Stack Shrinking
11:50 Matti Järvisalo and Armin Biere
Reconstructing Solutions after Blocked Clause Elimination
12:10 Ashish Sabharwal, Bart Selman and Lukas Kroc
An Empirical Study of Optimal Noise and Runtime Distributions in Local Search
14:00‑15:00 FLoC Plenary Talks: tribute to Amir and Robin
Chair: Moshe Vardi
Location: George Square Lecture Theatre
14:00 David Harel (Weizmann Institute of Science)
Amir Pnueli: A Gentle Giant, Lord of the Phi's and the Psi's.
14:30 Gordon Plotkin (University of Edinburgh)
Robin Milner, a Craftsman of Tools for the Mind.
15:30‑17:30 Theory + Combinatorics
Location: AT LT2
15:30 Kazuhisa Makino, Suguru Tamaki and Masaki Yamamoto
An Exact Algorithm for the Boolean Connectivity Problem for k-CNF
16:00 Hadi Katebi, Karem Sakallah and Igor Markov
Symmetry and Satisfiability: An Update
16:30 Stefan Porschen, Tatjana Schmidt and Ewald Speckenmeyer
Complexity Results for Linear XSAT Problems
17:00 Olaf Beyersdorff, Arne Meier, Sebastian Mueller, Michael Thomas and Heribert Vollmer
Proof Complexity of Propositional Default Logic
Monday, July 12th

Monday's program is also available with abstracts and side by side with other events.

09:00‑10:00 SAT Invited Talk
Location: AT LT2
09:00 Ramamohan Paturi.
Exact Algorithms and Complexity
10:30‑12:30 Theory + Combinatorics
Location: AT LT2
10:30 Evgeny Dantsin and Alexander Wolpert
On Moderately Exponential Time for SAT
11:00 Eli Ben-Sasson and Jan Johannsen
Lower bounds for width-restricted clause learning on small width formulas
11:30 Scott Cotton
Some Techniques for Minimizing Resolution Proofs
11:50 Allen Van Gelder and Ivor Spence
Zero-One Designs Produce Small Hard SAT Instances
12:10 William Matthews and Ramamohan Paturi
Uniquely Satisfiable k-SAT Instances with Almost Minimal Occurrences of Each Variable
14:00‑14:50 SAT Usage
Location: AT LT2
14:00 Carsten Fuhs and Peter Schneider-Kamp
Synthesizing Shortest Straight-Line Programs over GF(2) using SAT
14:30 Oliver Kullmann
Green-Tao Numbers and SAT
15:30‑17:20 QBF
Location: AT LT2
15:30 Uwe Bubeck and Hans Kleine Büning
Rewriting (Dependency-)Quantified 2-CNF with Arbitrary Free Literals into Existential 2-HORN
16:00 Christian Miller, Stefan Kupferschmid, Matthew Lewis and Bernd Becker
Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs
16:30 Enrico Giunchiglia, Paolo Marin and Massimo Narizzano
sQueezeBF: An effective preprocessor for QBFs
17:00 Alexandra Goultiaeva and Fahiem Bacchus
Exploiting Circuit Representations in QBF solving
Tuesday, July 13th

Tuesday's program is also available with abstracts and side by side with other events.

09:00‑10:00 FLoC Plenary Talk: Georg Gottlob
Chair: Martin Grohe
Location: George Square Lecture Theatre
09:00 Georg Gottlob (University of Oxford)
Datalog+-: A Family of Logical Query Languages for New Applications.
10:30‑12:30 Random + Statistics/LS
Location: AT LT2
10:30 Vishwambhar Rathi, Erik Aurell, Lars Rasmussen and Mikael Skoglund
Bounds on Threshold of Regular Random $k$-SAT
11:00 Thomas Hugel and Yacine Boufkhad
Non Uniform Selection of Solutions for Upper Bounding the 3-SAT Threshold
11:30 Mladen Nikolic
Statistical Methodology for Comparison of SAT Solvers
11:50 Adrian Balint and Andreas Fröhlich
Improving stochastic local search for SAT with instance specific information and a new probability distribution
12:10 Anton Belov and Zbigniew Stachniak
Improved Local Search for Circuit Satisfiability
14:00‑15:00 FLoC Keynote Talk: J Strother Moore
Chair: Jean-Pierre Jouannaud
Location: George Square Lecture Theatre
14:00 J Strother Moore (University of Texas)
Theorem Proving for Verification: The Early Days.
15:30‑17:00 QBF
Location: AT LT2
15:30 Robert Brummayer, Florian Lonsing and Armin Biere
Automated Testing and Debugging of SAT and QBF Solvers
16:00 William Klieber, Samir Sapra, Sicun Gao and Edmund Clarke
A Non-Prenex, Non-Clausal QBF Solver with Game-State Learning
16:30 Florian Lonsing and Armin Biere
Integrating Dependency Schemes in Search-Based QBF Solvers
17:00‑18:00 Business Meeting
Location: AT LT2
17:00 SAT Business meeting
Wednesday, July 14th

Wednesday's program is also available with abstracts and side by side with other events.

09:00‑10:00 SAT Invited Tutorial
Location: AT LT2
09:00 Daniel Kroening
A Primer on the Algorithmic Aspects of Satisfiability Modulo Theories
10:30‑12:30 Optimization + SAT Usage
Location: AT LT2
10:30 Vasco Manquinho, Ruben Martins and Inês Lynce
Improving Unsatisfiability-based Algorithms for Boolean Optimization
11:00 Denis Pankratov and Allan Borodin
On the Relative Merits of Simple Local Search Methods for the Max Sat Problem
11:30 Chu-Min LI, Felip Manya, Zhe Quan and Zhu Zhu
Exact MinSAT Solving
11:50 Rüdiger Ehlers
Minimising Deterministic Büchi Automata Precisely using SAT Solving
12:10 Gayathri Namasivayam and Mirosław Truszczynski
Simple but Hard Mixed Horn Formulas
14:00‑14:50 Joint SAT/SMT session
Location: AT LT2
14:00 Miquel Bofill, Josep Suy and Mateu Villaret
A system for solving constraint satisfaction problems with SMT
14:20 J. Christ, J. Hoenicke
(SMT'10) Instantiation-Based Interpolation for Quantified Formulae
15:30‑17:30 Competitions
Location: AT LT2
15:30 Claudia Peschiera, Luca Pulina, Armando Tacchella, Uwe Bubeck, Oliver Kullmann and Ines Lynce
The Seventh QBF Solvers Evaluation (QBFEVAL'10)
16:00 Competition
16:30 Competition
17:00 Competition