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.
Breaks:
- 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:00 | Lunch, 1st floor
|
|
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
[slides] |
|
(Introduction: Nadia Creignou) |
|
15:20-15:50 | Coffee, 4th floor lobby |
|
15:50-16:50 | Propositional 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:00 | Welcome Reception
Location: Lehtisali (entrance from the 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 [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:00 | Coffee, 4th floor lobby |
|
11:00-12:30 | Parallel 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:00 | Lunch, 1st floor
SAT Steering Committee Lunch Meeting (by invitation only, 2nd floor)
|
|
14:00-15:00 | Invited talk: Edmund M. Clarke
Turing's Computable Real Numbers and Why They Are
Still Important Today
[slides]
(Introduction: Armin Biere) |
|
15:00-15:30 | Coffee, 4th floor lobby |
|
15:30-16:50 | Maximum 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: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 [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:00 | Coffee, 4th floor lobby |
|
11:00-12:30 | Beyond 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:00 | Lunch, 1st floor |
|
14:00-15:00 | Invited talk: Peter Stuckey
There Are No CNF Problems [slides]
(Introduction: Allen Van Gelder)
|
|
15:00-15:30 | Coffee, 4th floor lobby |
|
15:30-16:30 | Solver 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:00 | Tool 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-23 | 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 [slides]
- QBF Gallery 2013 [slides]
- MaxSAT Evalutation 2013 [slides]
- Configurable SAT Solver Challenge 2013 [slides]
- SAT Competition 2013 [slides]
|
|
10:05-11:30 | Combined 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:30 | Clique-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:00 | Lunch, 1st floor |
|
14:00-15:00 | Propositional 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:50 | Parameterized 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-17 | Closing Ceremony, Drinks and cocktail snacks |