SAT 2013
16th International Conference on Theory and Applications of Satisfiability Testing

July 8-12, 2013   ·   Helsinki, Finland

SAT 2013 Conference Program

This program is ASCII text.

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, plus the demo/poster session

Monday July 8: Workshops 9:00-17:00

Registration opens at 8:30.

Please check the workshop websites for the detailed workshop programs.


  • 10:30-11:00 Coffee, 4th floor lobby
  • 12:30-14:00 Lunch, 1st floor
  • 15:00-15:30 Coffee, 4th floor lobby

Tuesday July 9

Registration opens at 8:45.

Morning 9:00-12:30: Workshops
Please check the workshop websites for the detailed workshop programs.

Morning coffee break: 10:30, 4th floor

12:30-14:00Lunch, 1st floor
14:00-14:20Welcome, best paper announcement
14:20-15:20Invited talk: Albert Atserias
The Proof-Search Problem between Bounded-Width Resolution and Bounded-Degree Semi-Algebraic Proofs [slides]
(Introduction: Nadia Creignou)
15:20-15:50Coffee, 4th floor lobby
15:50-16:50Propositional Proof Complexity I
(Session Chair: Stefan Szeider)
  • Exponential Separations in a Hierarchy of Clause Learning Proof Systems [slides]
    by Jan Johannsen
  • The Complexity of Theorem Proving in Autoepistemic Logic [slides]
    by Olaf Beyersdorff
18:00-20:00Welcome Reception
Location: Lehtisali (entrance from the Senate Square side)

Wednesday July 10

Registration opens at 8:45.

9:00-10:30Quantified Boolean Formulas
(Session Chair: Hans Kleine Buening)
  • On Propositional QBF Expansions and Q-Resolution [slides]
    by Mikolas Janota and Joao Marques-Silva
  • Recovering and Utilizing Partial Duality in QBF [slides]
    by Alexandra Goultiaeva and Fahiem Bacchus
  • Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation [slides]
    by Florian Lonsing, Uwe Egly and Allen Van Gelder
10:30-11:00Coffee, 4th floor lobby
11:00-12:30Parallel Solving
(Session Chair: Marijn Heule)
  • Soundness of Inprocessing in Clause Sharing SAT Solvers [slides]
    by Norbert Manthey, Tobias Philipp and Christoph Wernhard
  • Concurrent Clause Strengthening [slides]
    by Siert Wieringa and Keijo Heljanko
  • Parallel MUS Extraction [slides]
    by Anton Belov, Norbert Manthey and Joao Marques-Silva
12:30-14:00Lunch, 1st floor
SAT Steering Committee Lunch Meeting (by invitation only, 2nd floor)
14:00-15:00Invited talk: Edmund M. Clarke
Turing's Computable Real Numbers and Why They Are Still Important Today [slides]
(Introduction: Armin Biere)
15:00-15:30Coffee, 4th floor lobby
15:30-16:50Maximum Satisfiability
(Session Chair: Jordi Planes)
  • A Modular Approach to MaxSAT Modulo Theories [slides]
    by Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma and Roberto Sebastiani
  • Exploiting the Power of MIPs Solvers in Maxsat [slides]
    by Jessica Davies and Fahiem Bacchus
  • Community-based Partitioning for MaxSAT Solving (short paper) [slides]
    by Ruben Martins, Vasco Manquinho and Ines Lynce
17:00-18:00General Assembly of the SAT Association
(open to all conference participants)

Thursday July 11

Registration opens at 8:45.

9:00-10:30Encodings and Applications
(Session Chair: Roberto Sebastiani)
  • A Constraint Satisfaction Approach for Programmable Logic Detailed Placement [slides]
    by Andrew Mihal and Steve Teig
  • Nested Boolean Functions as Models for Quantified Boolean Formulas (short paper) [slides]
    by Uwe Bubeck and Hans Kleine Buening
  • Minimizing Models for Tseitin-Encoded SAT Instances (short paper) [slides]
    by Carsten Sinz, Markus Iser and Mana Taghdiri
  • Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction (short paper) [slides]
    by Gilles Audemard, Jean-Marie Lagniez and Laurent Simon
10:30-11:00Coffee, 4th floor lobby
11:00-12:30Beyond SAT
(Session Chair: Martina Seidl)
  • Solutions for Hard and Soft Constraints Using Optimized Probabilistic Satisfiability [slides]
    by Marcelo Finger, Carla Gomes, Ronan Le Bras and Bart Selman
  • Quantified Maximum Satisfiability: A Core-Guided Approach [slides]
    by Alexey Ignatiev, Mikolas Janota and Joao Marques-Silva
  • Experiments with Reduction Finding [slides]
    by Charles Jordan and Lukasz Kaiser
12:30-14:00Lunch, 1st floor
14:00-15:00Invited talk: Peter Stuckey
There Are No CNF Problems [slides]
(Introduction: Allen Van Gelder)
15:00-15:30Coffee, 4th floor lobby
15:30-16:30Solver Techniques and Analysis
(Session Chair: Alexander Nadel)
  • Factoring Out Assumptions to Speed Up MUS Extraction [slides]
    by Jean Marie Lagniez and Armin Biere
  • On the Interpolation between Product-Based Message Passing Heuristics for SAT [slides]
    by Oliver Gableske
*** Note: no break here ***

16:30-17:00Tool Paper Overviews
(Session Chair: Matti Järvisalo)
  • MUStICCa: MUS Extraction with Interactive Choice of Candidates [slides]
    by Johannes Dellert, Christian Zielke and Michael Kaufmann
  • LearnSAT: A SAT Solver for Education [slides]
    by Mordechai Moti Ben-Ari
  • SCSat: A Soft Constraint Guided SAT Solver [slides]
    Hiroshi Fujita, Miyuki Koshimura and Ryuzo Hasegawa
  • Snappy: A Simple Algorithm Portfolio [slides]
    by Horst Samulowitz, Chandra Reddy, Ashish Sabharwal and Meinolf Sellmann
  • Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems [slides]
    by Takehide Soh, Naoyuki Tamura and Mutsunori Banbara
  • 18-23Excursion and Conference Dinner

    Friday July 12

    Registration opens at 8:45.

    9:00-10:05Competition Overviews
    (Session Chair: Olivier Roussel)
    • SMT-EVAL 2013 [slides]
    • QBF Gallery 2013 [slides]
    • MaxSAT Evalutation 2013 [slides]
    • Configurable SAT Solver Challenge 2013 [slides]
    • SAT Competition 2013 [slides]
    10:05-11:30Combined tool demo and poster session, coffee
    (Location: 2nd floor lobby)

    Tool demos:
    • MUStICCa: MUS Extraction with Interactive Choice of Candidates
    • LearnSAT: A SAT Solver for Education
    • SCSat: A Soft Constraint Guided SAT Solver
    • Snappy: A Simple Algorithm Portfolio
    • Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems
    Presentation-only posters:
    • Probabilistic Satisfiability via Satisfiability Modulo Theory
      by Glauber De Bona and Marcelo Finger
    • Parallel SAT Solving with Search Space Partitioning
      by Ahmed Irfan, Davide Lanti and Norbert Manthey
    • On estimating total time to solve SAT in distributed computing environments: Application to the SAT@home project
      by Oleg Zaikin and Alexander Semenov
    • CSPSAT Projects and their SAT Related Tools
      by Naoyuki Tamura, Takehide Soh, Mutsunori Banbara, and Katsumi Inoue
    • A Novel, Efficient Approach for Enumerating MUSes
      by Mark Liffiton, Alessandro Previti, Ammar Malik, and Joao Marques-Silva
    • SAT Solvers in Computational Algorithm Design
      by Danny Dolev, Juho Hirvonen, Janne H. Korhonen, Christoph Lenzen, Joel Rybicki and Jukka Suomela
    • GlueMiniSat 2.2.7: On-The-Fly Lazy Clause Simplification
      by Hidetomo Nabeshima, Koji Iwanuma, and Katsumi Inoue
    Competition posters:
    • SMT-EVAL 2013
    • QBF Gallery 2013
    • MaxSAT Evalutation 2013
    • Configurable SAT Solver Challenge 2013
    • SAT Competition 2013
    11:30-12:30Clique-Width and SAT
    (Session Chair: John Franco)
    • A SAT Approach to Clique-Width [slides]
      by Marijn Heule and Stefan Szeider
    • Cliquewidth and Knowledge Compilation [slides]
      by Igor Razgon and Justyna Petke
    12:30-14:00Lunch, 1st floor
    14:00-15:00Propositional Proof Complexity II
    (Session Chair: Jan Johannsen)
    • A Rank Lower Bound for Cutting Planes Proofs of Ramsey's Theorem [slides]
      by Massimo Lauria
    • On the Resolution Complexity of Graph Non-Isomorphism [slides]
      by Jacobo Toran
    *** Note: no break here ***

    15:00-15:50Parameterized Complexity
    (Session Chair: Jakob Nordström)
    • Local Backbones [slides]
      by Ronald de Haan, Iyad Kanj and Stefan Szeider
    • Upper and Lower Bounds for Weak Backdoor Set Detection (short paper) [slides]
      by Neeldhara Misra, Sebastian Ordyniak, Venkatesh Raman and Stefan Szeider
    15:50-17Closing Ceremony, Drinks and cocktail snacks