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 |
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 |