Thursday, May 2, 2013

[DMANET] SAT 2013 Call for Participation

[ We apologize if you receive multiple copies of this call. ]
-------------------------------------------------------------------------

CALL FOR PARTICIPATION

Sixteenth International Conference on
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
--- SAT 2013 ---

Helsinki, Finland, July 8-12, 2013
http://sat2013.cs.helsinki.fi/

***** REGISTRATION TO SAT 2013 IS NOW OPEN AT *****
***** http://sat2013.cs.helsinki.fi/registration.html *****
***** *****
***** EARLY REGISTRATION DEADLINE: May 27, 2013 *****

-------------------------------------------------------------------------

SAT 2013 CONFERENCE HIGHLIGHTS
==============================

-Three high-quality INVITED TALKS:
+Albert Atserias:
"The Proof-Search Problem between Bounded-Width Resolution and
Bounded-Degree Semi-Algebraic Proofs"
+Edmund M. Clarke:
"Turing's Computable Real Numbers and Why They Are Still Important
Today"
+Peter Stuckey:
"There are no CNF problems"

-Around 30 SCIENTIFIC TALKS on SAT 2013 accepted papers, see full list
below.

-WORKSHOPS:
SMT 2013: 1th International Workshop on Satisfiability Modulo Theories
PoS 2013: 4th International Workshop on Pragmatics of SAT
QBF 2013: International Workshop on Quantified Boolean Formulas

-COMPETITIONS AND SYSTEM EVALUATIONS:
SAT Competition 2013
Configurable SAT Solver Challenge 2013
Max-SAT Evaluation 2013
SMT-EVAL 2013
QBF Gallery 2013

SAT 2013 ACCEPTED PAPERS
========================

Gilles Audemard, Jean-Marie Lagniez and Laurent Simon:
On Improving SAT Engines for Incremental SAT Solving with
Assumptions.

Anton Belov, Norbert Manthey and Joao Marques-Silva:
Parallel MUS Extraction.

Olaf Beyersdorff:
The Complexity of Theorem Proving in Autoepistemic Logic.

Uwe Bubeck and Hans Kleine Büning:
Nested Boolean Functions as Models for Quantified Boolean Formulas.

Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma and
Roberto Sebastiani:
A Modular Approach to MaxSAT Modulo Theories.

Jessica Davies and Fahiem Bacchus:
Exploiting the Power of MIPs Solvers in Maxsat.

Ronald de Haan, Iyad Kanj and Stefan Szeider:
Local Backbones.

Johannes Dellert, Christian Zielke and Michael Kaufmann:
MUStICCa: MUS Extraction with Interactive Choice of Candidates
(Tool paper).

Marcelo Finger, Carla Gomes, Ronan Le Bras and Bart Selman:
Solutions for Hard and Soft Constraints Using Optimized
Probabilistic Satisfiability.

Hiroshi Fujita, Miyuki Koshimura and Ryuzo Hasegawa:
SCSat: A Soft Constraint Guided SAT Solver (Tool paper).

Oliver Gableske:
On the Interpolation between Product-Based Message Passing
Heuristics for SAT.

Alexandra Goultiaeva and Fahiem Bacchus:
Recovering and Utilizing Partial Duality in QBF.

Marijn Heule and Stefan Szeider:
A SAT Approach to Clique-Width.

Alexey Ignatiev, Mikolas Janota and Joao Marques-Silva:
Quantified Maximum Satisfiability: A Core-Guided Approach.

Mikolas Janota and Joao Marques-Silva:
On Propositional QBF Expansions and Q-Resolution.

Jan Johannsen:
Exponential Separations in a Hierarchy of Clause Learning Proof
Systems.

Charles Jordan and Lukasz Kaiser:
Experiments with Reduction Finding.

Massimo Lauria:
A rank lower bound for cutting planes proofs of Ramsey's Theorem.

Florian Lonsing, Uwe Egly and Allen Van Gelder:
Efficient Clause Learning for Quantified Boolean Formulas via QBF
Pseudo Unit Propagation.

Norbert Manthey, Tobias Philipp and Christoph Wernhard:
Soundness of Inprocessing in Clause Sharing SAT Solvers.

Jean Marie Lagniez and Armin Biere:
Factoring-Out Assumptions to Speed-Up MUS Extraction.

Ruben Martins, Vasco Manquinho and Inês Lynce:
Community-based Partitioning for MaxSAT Solving.

Andrew Mihal and Steve Teig:
A Constraint Satisfaction Approach for Programmable Logic Detailed
Placement.

Neeldhara Misra, Sebastian Ordyniak, Venkatesh Raman and Stefan
Szeider:
Upper and Lower Bounds for Weak Backdoor Set Detection.

Mordechai Moti Ben-Ari:
LearnSAT: A SAT Solver for Education (Tool paper).

Igor Razgon and Justyna Petke:
Cliquewidth and Knowledge Compilation.

Horst Samulowitz, Chandra Reddy, Ashish Sabharwal and Meinolf
Sellmann:
Snappy: A Simple Algorithm Portfolio (Tool paper).

Carsten Sinz, Markus Iser and Mana Taghdiri:
Minimizing Models for Tseitin-Encoded SAT Instances.

Takehide Soh, Naoyuki Tamura and Mutsunori Banbara:
Scarab: A Rapid Prototyping Tool for SAT-based Constraint
Programming Systems (Tool paper).

Jacobo Toran:
On the resolution complexity of Graph non-Isomorphism.

Siert Wieringa and Keijo Heljanko:
Concurrent clause strengthening.


SAT 2013 VENUE
==============

SAT 2013 takes place in Helsinki, the capital of Finland, a vibrant
scandinavian and international city that is easily access from various
destinations within Europe and around the world. SAT 2013 is organized
at
University of Helsinki in the very heart of the city. SAT 2013 takes
place
during the main summer season, allowing one to experience the
whitenights
during which the sun almost never sets.

**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************