Conference Programme

Summary


	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


	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


	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


	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