Our sponsors


June 29, 2011 Old pages moved, Photos added

June 13, 2011 Additional directions to housing added

June 2, 2011 lodging at Baits is full

May 3, 2011 Conference Schedule added

Apr 15, 2011 Final list of accepted papers added

Apr 4, 2011 Accommodation / Registration Opened

Feb 17,2011: MaxSAT Evaluation Deadline Added

Feb 16, 2011: Extended Deadline for paper submissions (21st instead of 18th, Feb).

Dec 20, 2010: Final CFP Added

Sep 24, 2010: Preliminary CFP Added

Aug 31, 2010: Web Site opens


Workshops proposals
Dec. 17, 2010

Abstract submission
Feb. 11, 2011

Paper submission
Feb. 21, 2011

Author notification
Mar. 20, 2011

Final version
Apr. 8, 2011

June 19th to 22th, 2011

June 18th and 23th, 2011

Affiliated Events Main Dates

SAT Competition
Web site
Bench. Submission:
Feb. 13, 2011
Solver Submission:
(ext.) March 2, 2011

PB Evaluation
Web Site
Solver/Benchs. Subm.:
March 20, 2011

MAX-SAT Evaluation
Web Site
Solver Submission:
March 25, 2011

Affiliated Workshops Main Dates

web site
Abstract: April, 10th
Papers: April, 17th

web site
Abstract: April, 22nd
Papers: April, 29th

web site
Abstract: April, 17th
Papers: April, 24th

SAT/SMT Solver Summer School 2011

The SAT 2011 conference is held just a few days after the SAT/SMT Solver Summer School 2011 (from June 12th to June 17th), located at MIT, Cambridge, USA.

Conference Schedule

Saturday 6/18/2011

5:00 PM -- 7:00 PM: Reception

Sunday 6/19/2011

8:00 AM -- 9:00 AM


9:00 AM -- 9:30 AM


9:30 AM -- 11:30 AM: Session 1: Complexity Analysis

Satisfiability Certificates Verifiable in Subexponential Time (BP)
Evgeny Dantsin and Edward A. Hirsch

Satisfiability of Acyclic and Almost Acyclic CNF Formulas (II)
Sebastian Ordyniak, Daniel Paulusma and Stefan Szeider

How to apply SAT-solving for the equivalence test of monotone normal forms
Martin Mundhenk and Robert Zeranski

Parameterized Complexity of DPLL Search Procedures (BP)
Olaf Beyersdorff, Nicola Galesi and Massimo Lauria

11:30 AM -- 12:30 PM


12:30 PM -- 2:00 PM: Session 2: Binary Decision Diagrams

PiDD: A New Decision Diagram for Efficient Problem Solving in Permutation Space
Shin-Ichi Minato

DPLL+ROBDD Derivation Applied to Inversion of Some Cryptographic Functions
Alexey Ignatiev and Alexander Semenov

BDDs for Pseudo-Boolean Constraints – Revisited
Ignasi Abio, Robert Nieuwenhuis, Albert Oliveras and Rodriguez-Carbonell Enric

2:00 PM -- 2:30 PM


2:30 PM -- 4:00 PM: Poster Sessions*

Translating Pseudo-Boolean Constraints into CNF
Amir Aavani

Experimenting with the Instances of the MaxSAT Evaluation
Josep Argelich, Chu Min Li, Felip Manya and Jordi Planes

Model Counting Using the Inclusion-Exclusion Principle.
Huxley Bennett and Sriram Sankaranarayanan

Phase Transitions in Knowledge Compilation: an Experimental Study
Jian Gao, Minghao Yin and Ke Xu

EagleUP: Solving Random 3-SAT using SLS with Unit Propagation
Oliver Gableske and Marijn Heule

Non-Model-Based Algorithm Portfolios for SAT
Yuri Malitsky, Ashish Sabharwal, Horst Samulowitz and Meinolf Sellmann

The order encoding: from tractable CSP to tractable SAT
Justyna Petke and Peter Jeavons

Applying UCT to Boolean Satisfiability
Alessandro Previti, Raghuram Ramanujan, Marco Schaerf and Bart Selman

A Compact and Efficient SAT-encoding of Finite Domain CSP
Tomoya Tanjo, Naoyuki Tamura and Mutsunori Banbara

Learning Polarity from Structure in SAT
Bryan Silverthorn and Risto Miikkulainen

(*) posters will be kept during all conference

4:00 PM -- 5:30 PM: Session 3: Empirical Evaluation and SAT Competition 2011 Preview

Generalized Conflict-Clause Strengthening for Satisfiability Solvers
Allen Van Gelder

SAT Competition 2011 Preview and First Phase Analysis (presentation)
Daniel Le Berre, Olivier Roussel and Matti Jarvisalo

Careful Ranking of Multiple Solvers with Timeouts and Ties
Allen Van Gelder

6:00 PM -- 7:30 PM


Monday 6/20/2011

8:00 AM -- 9:00 AM


9:00 AM -- 10:00 AM: Invited Talk 1

Ryan Williams
Connecting SAT Algorithms and Complexity Lower Bounds

10:00 AM -- 10:30 AM


10:30 AM -- 12:00 PM: Session 4: Theoretical Analysis

A Satisfiability-based Approach for Embedding Generalized Tanglegrams on Level Graphs
Ewald Speckenmeyer, Andreas Wotzlaw and Stefan Porschen

Enumerating All Solutions of a Boolean CSP by Non-Decreasing Weight
Johannes Schmidt, Nadia Creignou and Frederic Olive

On variables with few occurrences in conjunctive normal forms
Oliver Kullmann and Xishun Zhao

12:00 PM -- 1:00 PM


1:00 PM -- 2:30 PM: Session 5: Extraction of Minimal Unsatisfiable Subsets

Minimally Unsatisfiable Boolean Circuits
Anton Belov and Joao Marques-Silva

Faster Extraction of High-Level Minimal Unsatisfiable Cores
Vadim Ryvchin and Ofer Strichman

On Improving MUS Extraction Algorithms
Joao Marques-Silva and Ines Lynce

2:30 PM -- 3:00 PM


3:00 PM -- 4:30 PM: Panel Discussion

Topic: Establishing Standards for Empirical Evaluations
Moderator: Allen Van Gelder
Panel Members: Armin Biere
Marijn Heule
Laurent Simon

4:30 PM -- 6:00 PM

Business Meeting

Tuesday 6/21/2011

8:00 AM -- 8:30 AM


8:30 AM -- 9:30 AM: Invited Talk 2

Koushik Sen
Concolic Testing and Constraint Satisfaction

9:30 AM -- 10:00 AM


10:00 AM -- 12:00 PM: Session 6: SAT Algorithms

On Freezing and Reactivating Learnt Clauses (BP)
Gilles Audemard, Jean Marie Lagniez, Bertrand Mazure and Lakdhar Sais

Efficient CNF Simplification based on Binary Implication Graphs
Marijn Heule, Matti Jarvisalo and Armin Biere

Between Restarts and Backjumps
Antonio Ramos, Peter Van Der Tak and Marijn Heule

Captain Jack: New Variable Selection Heuristics in Local Search for SAT
Dave Tompkins, Adrian Balint and Holger Hoos

12:00 PM -- Late

Social Event

Wednesday 6/22/2011

8:00 AM -- 9:00 AM


9:00 AM -- 10:30 AM: Session 7: Quantified Boolean Formulae

Failed Literal Detection for QBF
Florian Lonsing and Armin Biere

Abstraction-Based Algorithm for 2QBF
Mikolas Janota and Joao Marques-Silva

Transformations into Normal Forms for Quantified Circuits
Hans Kleine Buning, Xishun Zhao and Uwe Bubeck

10:30 AM -- 11:00 AM


11:00 AM -- 12:30 PM: Session 8: Model Enumeration, Empirical Study

Generating Diverse Solutions in SAT
Alexander Nadel

Reducing Chaos in SAT-like Search: Finding Solutions Close to a Given One
Ignasi Abio, Morgan Deters, Robert Nieuwenhuis and Peter Stuckey

Empirical Study of the Anatomy of Modern SAT Solvers
Hadi Katebi, Karem A. Sakallah and Joao Marques-Silva

12:30 PM -- 1:30 PM


1:30 PM -- 3:00 PM

Competitions results and discussion (SAT, MAXSAT, PB)

3:00 PM -- 3:30 PM

Best Papers & Closing