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.

Technical Program

Full papers

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

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

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

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

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

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

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

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

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

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

Minimally Unsatisfiable Boolean Circuits
Anton Belov and Joao Marques-Silva

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

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

On Freezing and Reactivating Learnt Clauses
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

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

Failed Literal Detection for QBF
Florian Lonsing and Armin Biere

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

Generating Diverse Solutions in SAT
Alexander Nadel

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

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

Generalized Conflict-Clause Strengthening for Satisfiability Solvers
Allen Van Gelder

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

Extended Abstracts

Translating Pseudo-Boolean Constraints into CNF
Amir Aavani

Experimenting with the Instances of the MaxSAT Evaluation
Josep Argelich, Chu Min Li, Felip Many\`a 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