SAT 2013 Conference Program 16th International Conference on Theory and Applications of Satisfiability Testing July 8-12, 2013, Helsinki, Finland http://sat2013.cs.helsinki.fi/ ----------------------------------------------------------------------------- LENGTHS OF PRESENTATIONS Regular papers: 25 min + 5 min for questions Short papers: 15 min + 5 min for questions Tool papers: 5 min + 1 min, questions during demo/poster session ----------------------------------------------------------------------------- MONDAY July 8 Registration opens at 8:30. 9:00-17:00: Workshops SMT 2013: 11th International Workshop on Satisfiability Modulo Theories PoS 2013: 4th International Workshop on Pragmatics of SAT Breaks: 10:30-11:00 Coffee 12:30-14:00 Lunch 15:00-15:30 Coffee ----------------------------------------------------------------------------- TUESDAY July 9, Morning Registration opens at 8:45. 9:00-12:30: Workshops SMT 2013: 11th International Workshop on Satisfiability Modulo Theories QBF 2013: International Workshop on Quantified Boolean Formulas ----------------------------------------------------------------------------- TUESDAY July 9, Afternoon 12:30-14:00 Lunch 14:00-14:20 Welcome, best paper announcement 14:20-15:20 Invited talk: Albert Atserias "The Proof-Search Problem between Bounded-Width Resolution and Bounded-Degree Semi-Algebraic Proofs" (Introduction: Nadia Creignou) 15:20-15:50 Coffee 15:50-16:50 Propositional Proof Complexity I (Session Chair: Stefan Szeider) -Exponential Separations in a Hierarchy of Clause Learning Proof Systems by Jan Johannsen -The Complexity of Theorem Proving in Autoepistemic Logic by Olaf Beyersdorff 18:00-20:00 Social program: Welcome Reception (Location: Lehtisali, entrance from Senate Square side) ----------------------------------------------------------------------------- WEDNESDAY July 10 Registration opens at 8:45. 9:00-10:30 Quantified Boolean Formulas (Session Chair: Hans Kleine Buening) -On Propositional QBF Expansions and Q-Resolution by Mikolas Janota and Joao Marques-Silva -Recovering and Utilizing Partial Duality in QBF by Alexandra Goultiaeva and Fahiem Bacchus -Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation by Florian Lonsing, Uwe Egly and Allen Van Gelder 10:30-11:00 Coffee 11:00-12:30 Parallel Solving (Session Chair: Marijn J.H. Heule) -Soundness of Inprocessing in Clause Sharing SAT Solvers by Norbert Manthey, Tobias Philipp and Christoph Wernhard -Concurrent Clause Strengthening by Siert Wieringa and Keijo Heljanko -Parallel MUS Extraction by Anton Belov, Norbert Manthey and Joao Marques-Silva 12:30-14:00 Lunch SAT Steering Committee Lunch Meeting (by invitation only) 14:00-15:00 Invited talk: Edmund M. Clarke "Turing's Computable Real Numbers and Why They Are Still Important Today" (Introduction: Armin Biere) 15:00-15:30 Coffee 15:30-16:50 Maximum Satisfiability (Session Chair: Jordi Planes) -A Modular Approach to MaxSAT Modulo Theories by Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma and Roberto Sebastiani -Exploiting the Power of MIPs Solvers in Maxsat by Jessica Davies and Fahiem Bacchus -Community-based Partitioning for MaxSAT Solving (short paper) by Ruben Martins, Vasco Manquinho and Ines Lynce 17:00-18:00 General Assembly of the SAT Association (open to all conference participants) ------------------------------------------------------------------------------- THURSDAY July 11 Registration opens at 8:45. 9:00-10:30 Encodings and Applications (Session Chair: Roberto Sebastiani) -A Constraint Satisfaction Approach for Programmable Logic Detailed Placement by Andrew Mihal and Steve Teig -Nested Boolean Functions as Models for Quantified Boolean Formulas (short paper) by Uwe Bubeck and Hans Kleine Buening -Minimizing Models for Tseitin-Encoded SAT Instances (short paper) by Carsten Sinz, Markus Iser and Mana Taghdiri -Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction (short paper) by Gilles Audemard, Jean-Marie Lagniez and Laurent Simon 10:30-11:00 Coffee 11:00-12:30 Beyond SAT (Session Chair: Martina Seidl) -Solutions for Hard and Soft Constraints Using Optimized Probabilistic Satisfiability by Marcelo Finger, Carla Gomes, Ronan Le Bras and Bart Selman -Quantified Maximum Satisfiability: A Core-Guided Approach by Alexey Ignatiev, Mikolas Janota and Joao Marques-Silva -Experiments with Reduction Finding by Charles Jordan and Lukasz Kaiser 12:30-14:00 Lunch 14:00-15:00 Invited talk: Peter Stuckey "There Are No CNF Problems" (Introduction: Allen Van Gelder) 15:00-15:30 Coffee 15:30-16:30 Solver Techniques and Analysis (Session Chair: Alexander Nadel) -Factoring Out Assumptions to Speed Up MUS Extraction by Jean Marie Lagniez and Armin Biere -On the Interpolation between Product-Based Message Passing Heuristics for SAT by Oliver Gableske *** Note: no break here *** 16:30-17:00 Tool Paper Overviews (Session Chair: Matti Jarvisalo) -MUStICCa: MUS Extraction with Interactive Choice of Candidates by Johannes Dellert, Christian Zielke and Michael Kaufmann: -LearnSAT: A SAT Solver for Education by Mordechai Moti Ben-Ari -SCSat: A Soft Constraint Guided SAT Solver Hiroshi Fujita, Miyuki Koshimura and Ryuzo Hasegawa -Snappy: A Simple Algorithm Portfolio by Horst Samulowitz, Chandra Reddy, Ashish Sabharwal and Meinolf Sellmann -Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems by Takehide Soh, Naoyuki Tamura and Mutsunori Banbara Around 18-23: Social Program: Excursion and Conference Dinner ------------------------------------------------------------------------------ FRIDAY July 12 Registration opens at 8:45. 9:00-10:05 Competition Overviews (Session Chair: Olivier Roussel) -SMT-EVAL 2013 (10 min) -QBF Gallery 2013 (10 min) -MaxSAT Evalutation 2013 (10 min) -Configurable SAT Solver Challenge 2013 (10 min) -SAT Competition 2013 (25 min) 10:05-11:30 Combined tool demo and poster session, coffee (Location: 2nd floor lobby) 11:30-12:30 Clique-Width and SAT (Session Chair: John Franco) -A SAT Approach to Clique-Width by Marijn Heule and Stefan Szeider -Cliquewidth and Knowledge Compilation by Igor Razgon and Justyna Petke 12:30-14:00 Lunch 14:00-15:00 Propositional Proof Complexity II (Session Chair: Jan Johannsen) -A Rank Lower Bound for Cutting Planes Proofs of Ramsey's Theorem by Massimo Lauria -On the Resolution Complexity of Graph Non-Isomorphism by Jacobo Toran *** Note: no break here *** 15:00-15:50 Parameterized Complexity (Session Chair: Jakob Nordstrom) -Local Backbones by Ronald de Haan, Iyad Kanj and Stefan Szeider -Upper and Lower Bounds for Weak Backdoor Set Detection (short paper) by Neeldhara Misra, Sebastian Ordyniak, Venkatesh Raman and Stefan Szeider 15:50-17: Closing Ceremony, Drinks and cocktail snacks