17th International Conference on Theory and Applications of Satisfiability Testing

July 14-17, 2014   ·   Vienna, Austria


For the program of pre-/post-conference workshops see the respective workshop pages.

Monday  Tuesday  Wednesday  Thursday 

Monday, July 14

08:45-09:15Session 37Chair: Agata Ciabattoni
VSL Opening Location: EI, EI 7 (video: EI, EI 9; EI, EI 10; FH, Hörsaal 1)
08:45-08:50Sabine Seidler Welcome Address by the Rector
08:50-08:55Matthias Baaz, Thomas Eiter and Helmut Veith Welcome Address by the Organizers
08:55-09:15Dana Scott VSL Opening
09:15-10:15Session 38Chair: Georg Gottlob
VSL Keynote Talk Location: EI, EI 7 (video: EI, EI 9; EI, EI 10; FH, Hörsaal 1)
09:15-10:15Christos Papadimitriou Computational Ideas and the Theory of Evolution
10:15-10:45Coffee Break
10:45-12:10Session 38EChair: Joao Marques-Silva
Maximum Satisfiability Location: FH, Hörsaal 6
10:45-10:50Uwe Egly and Carsten Sinz SAT Opening
10:50-11:20Takayuki Sakai, Kazuhisa Seto and Suguru Tamaki Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction
11:20-11:50Jan Arne Telle, Sigve Hortemo Sæther and Martin Vatshelle Solving MaxSAT and #SAT on structured CNF formulas
11:50-12:10Fahiem Bacchus and Nina Narodytska Cores in Core based MaxSat Algorithms: an Analysis
12:10-13:00Session 40Chair: Tobias Schubert
Minimal Unsatisfiability Location: FH, Hörsaal 6
12:10-12:40Alessandro Previti and Joao Marques-Silva On Computing Preferred MUSes and MCSes
12:40-13:00Anton Belov, Marijn Heule and Joao Marques-Silva MUS Extraction using Clausal Proofs
13:00-14:30Lunch Break
14:30-15:50Session 41DChair: Olaf Beyersdorff
Complexity and Reductions Location: FH, Hörsaal 6
14:30-15:00Ronald de Haan and Stefan Szeider Fixed-parameter tractable reductions to SAT
15:00-15:30Alexey Ignatiev, Antonio Morgado and Joao Marques-Silva On Reducing Maximum Independent Set to Minimum Satisfiability
15:30-15:50Matti Järvisalo and Janne H. Korhonen Conditional Lower Bounds for Failed Literals and Related Techniques
15:50-16:30Coffee Break
16:30-17:50Session 42EChair: Karem Sakallah
Tool Papers Location: FH, Hörsaal 6
16:30-16:50Charles Jordan, Lukasz Kaiser, Florian Lonsing and Martina Seidl MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing
16:50-17:10Nathan Wetzler, Marijn Heule and Warren Hunt DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
17:10-17:30Carles Creus, Pau Fernández and Guillem Godoy Automatic Evaluation of Reductions between NP-complete Problems
17:30-17:50Ruben Martins, Vasco Manquinho and Ines Lynce Open-WBO: a Modular MaxSAT Solver
20:00-21:30Session 44
VSL Opening Reception Location: Rathaus

Tuesday, July 15

08:45-10:15Session 44Chair: Moshe Vardi
FLoC Plenary Talk Location: FH, Hörsaal 1
08:45-10:15Orna Kupfermann From Reachability to Temporal Specifications in Game Theory
10:15-10:45Coffee Break
10:45-11:45Session 47FChair: Oliver Kullmann
Proof Complexity I Location: FH, Hörsaal 6
10:45-11:15Mladen Miksa and Jakob Nordström Long Proofs of (Seemingly) Simple Formulas
11:15-11:45Gabriel Istrate and Adrian Craciun Proof complexity and the Lovasz-Kneser Theorem
11:50-13:00Session 49Chair: Armin Biere
Parallel and Incremental (Q)SAT Location: FH, Hörsaal 6
11:50-12:20Alexander Nadel, Ofer Strichman and Vadim Ryvchin Ultimately Incremental SAT
12:20-12:40Tomohiro Sonobe, Shuya Kondoh and Mary Inaba Community Branching for Parallel Portfolio SAT Solvers
12:40-13:00Laurent Simon and Gilles Audemard Lazy clause exchange policy for parallel SAT solvers
13:00-14:30Lunch Break
13:00-14:30SAT Association SAT Steering Committee Meeting (by invitation only)
14:30-15:30Session 50FChair: Stefan Szeider
SAT Invited Talk I Location: FH, Hörsaal 6
14:30-15:30Jakob Nordström A (Biased) Proof Complexity Survey for SAT Practitioners
15:30-16:00Session 51Chair: Nadia Creignou
Proof Complexity II / 1 Location: FH, Hörsaal 6
15:30-16:00Oliver Kullmann and Olaf Beyersdorff Unified characterisations of resolution hardness measures
16:00-16:30Coffee Break
16:30-17:00Session 52EChair: Nadia Creignou
Proof Complexity II / 2 Location: FH, Hörsaal 6
16:30-17:00Valeriy Balabanov, Magdalena Widl and Jie-Hong Roland Jiang QBF Resolution Systems and their Proof Complexities
17:00-18:00Session 53
SAT Association General Assembly Location: FH, Hörsaal 6
19:00-20:00Session 56A
VSL Public Lecture 1 Location: MB, Kuppelsaal
19:00-20:00Karl Sigmund Gödel in Vienna
19:30-22:30SAT Association SAT SC+PC Dinner (by invitation only)

Wednesday, July 16

08:45-10:15Session 57Chair: Mathias Baaz
VSL Keynote Talk Location: EI, EI 7 (video: EI, EI 9; EI, EI 10; FH, Hörsaal 1)
08:45-10:15Alex Wilkie The theory and applications of o-minimal structures
10:15-10:45Coffee Break
10:45-11:55Session 56EChair: John Franco
Applications Location: FH, Hörsaal 6
10:45-11:05Boris Konev and Alexei Lisitsa A SAT Attack on the Erdos Discrepancy Conjecture
11:05-11:35Tamir Heyman, Dan Smith, Lance Leong, Husam Husam and Yogesh Mahajan Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
11:35-11:55Bernd Finkbeiner and Leander Tentrup Fast DQBF Refutation
12:00-13:00Session 58Chair: Marijn Heule
Structure Location: FH, Hörsaal 6
12:00-12:30Friedrich Slivovsky and Stefan Szeider Variable Dependencies and Q-Resolution
12:30-13:00Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard and Laurent Simon Impact of Community Structure on SAT Solver Performance BEST STUDENT PAPER AWARD
13:00-14:30Lunch Break
14:30-15:30Session 59EChair: Roberto Sebastiani
SAT Invited Talk II Location: FH, Hörsaal 6
14:30-15:30Leonardo De Moura A Model-Constructing Satisfiability Calculus
15:30-16:00Session 60Chair: Roberto Sebastiani
Simplifications, Solving I / 1 Location: FH, Hörsaal 6
15:30-16:00Adrian Balint, Armin Biere, Andreas Fröhlich and Uwe Schöning Efficient implementation of SLS solvers and new heuristics for k-SAT with long clauses
16:00-16:30Coffee Break
16:30-18:00Session 61EChair: Matti Järvisalo
Simplifications, Solving I / 2 Location: FH, Hörsaal 6
16:30-17:00Tomás Balyo, Andreas Fröhlich, Marijn Heule and Armin Biere Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask)
17:00-17:30Yoav Fekete and Michael Codish Simplifying Pseudo-Boolean Constraints in Residual Number Systems
17:30-18:00Armin Biere, Daniel Le Berre, Emmanuel Lonca and Norbert Manthey Detecting cardinality constraints in CNF
19:00-21:30Session 64
VSL Banquet Location: Schönbrunn

Thursday, July 17

08:45-10:15Session 62AChair: Moshe Vardi
FLoC Panel Location: FH, Hörsaal 1
08:45-10:15Nina Amla, Georg Gottlob, Falk Reckling, Sweitze Roffel and Andrei Voronkov Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change?
10:15-10:45Coffee Break
10:45-11:15Session 66AFChair: Laurent Simon
Simplifications and Solving II Location: FH, Hörsaal 6
10:45-11:15Daniel Larraz, Albert Oliveras, Enric Rodríguez Carbonell and Albert Rubio Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions
11:15-12:45Session 69Chair: Hans Kleine Büning
Analysis Location: FH, Hörsaal 6
11:15-11:45Oliver Gableske An Ising Model inspired Extension of the Product-based MP Framework for SAT
11:45-12:15Andrei Bulatov and Cong Wang Approximating highly satisfiable random 2-SAT
12:15-12:45Florent Capelli, Arnaud Durand and Stefan Mengel Hypergraph Acyclicity and Propositional Model Counting
13:00-14:30Lunch Break
14:30-16:00Session 75AFChair: Daniel Le Berre
Report on Competitions Location: FH, Hörsaal 6
14:30-14:50Josep Argelich, Chu Min Li, Felip Manya and Jordi Planes MaxSAT Evaluation
14:50-15:10Charles Jordan, Martina Seidl QBF Gallery
15:10-15:30Frank Hutter, Marius Lindauer, Sam Bayless, Holger Hoos and Kevin Leyton-Brown Configurable SAT Solver Challenge
15:30-15:55Anton Belov, Daniel Diepold, Matti Järvisalo and Marijn Heule SAT Competition 2014
15:55-16:00Uwe Egly and Carsten Sinz SAT Closing
16:00-16:30Coffee Break
16:30-19:00Session 79AChair: Matthias Baaz
VSL Joint Award Ceremony Location: MB, Kuppelsaal
16:30-17:30Kurt Gödel Research Prize Fellowships Program Foundations and Technology Competitions Award Ceremony
17:30-18:15Floc Olympic Games FLoC Olympic Games Award Ceremony
18:15-19:00Helmut Veith FLoC Closing Week 1
21:00-24:00Session 89
VSL Student Reception Location: will be announced