Thursday, May 23, 2013

[DMANET] SAT 2013 early registration reminder

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

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

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

***** EARLY REGISTRATION DEADLINE: May 27, 2013 *****
Early registration fees: 150 EUR for students
320 EUR regular

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

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.

**********************************************************
*
* 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/
*
**********************************************************