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

-------------------------------------------------------------------------
                  15th International Conference on 
        THEORY AND APPLICATIONS OF SATISFIABILITY TESTING 
                        --- SAT 2012 ---

                 Trento, Italy, June 17-20th, 2012
                      http://sat2012.fbk.eu/
-------------------------------------------------------------------------

AIM and SCOPE
=============

The International Conference on Theory and Applications of
Satisfiability Testing (SAT) is the primary annual meeting for
researchers studying the propositional satisfiability
problem. Importantly, here SAT is interpreted in a rather broad sense:
besides plain propositional satisfiability, it includes the domains of
MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean
Formulae (QBF), Satisfiability Modulo Theories (SMT), Constraints
Programming (CSP) techniques for word-level problems and their
propositional encoding.

To this extent, many hard combinatorial problems can be encoded as SAT
instances, in the broad sense mentioned above, including problems that
arise in hardware and software verification, AI planning and
scheduling, OR resource allocation, etc. The theoretical and practical
advances in SAT research over the past twenty years have contributed
to making SAT technology an indispensable tool in these domains.

SAT 2012 will take place in Trento, Italy, a cosmopolitan city set in
a spectacular mountain scenery, and home to a world-class university
and research centres.

RELEVANT TOPICS 
===============

The topics of the conference span practical and theoretical research
on SAT (in the broader sense above) and its applications, and include,
but are not limited to: 

* Theoretical issues
  - Combinatorial Theory of SAT
  - Proof Systems and Proof Complexity in SAT
  - Analysis of SAT Algorithms
* Solving: 
  - Improvements of current solving procedures
  - Novel solving procedures, techniques and heuristics
  - Incremental solving
* Beyond solving:
  - Functionalities (e.g., proofs, unsat-cores, interpolants,...)
  - Optimization 
* Applications 
  - SAT techniques for other domains
  - Novel Problem Encodings
  - Novel Industrial Applications of SAT

A more detailed description can be found on the web site.

INVITED SPEAKERS
================

We are honored to announce the following invited speakers at SAT 2012:

* Aaron Bradley, Boulder, USA. 
  "SAT-based Verification with IC3: Foundations and Demands"

* Donald Knuth, Stanford, USA.
  "Satisfiability and The Art of Computer Programming"

The presence of both speakers has been confirmed, although the titles
 of the talks may be provisional.

AFFILIATED EVENTS
=================

SAT 2012 is co-located with the 2nd International SAT/SMT Summer School
(June 12-15), http://satsmtschool2012.fbk.eu/.

SAT 2012 will also host related events like workshops (June 16) and various
competitive events.

PAPER SUBMISSION
================

Papers must be edited in LATEX using the LNCS format and
be submitted electronically as PDF files via EasyChair. 
We envisage three categories of submissions:

REGULAR PAPERS. Submissions, not exceeding fourteen (14) pages, should
  contain original research, and sufficient detail to assess the
  merits and relevance of the contribution. For papers reporting
  experimental results, authors are strongly encouraged to make their
  data available with their submission. Submissions reporting on case
  studies in an industrial context are strongly invited, and should
  describe details, weaknesses and strength in sufficient
  depth. Simultaneous submission to other conferences with proceedings
  or submission of material that has already been published elsewhere
  is not allowed.

TOOL PRESENTATIONS. Submissions, not exceeding six (6) pages, should
  describe the implemented tool and its novel features. A
  demonstration is expected to accompany a tool presentation. Papers
  describing tools that have already been presented in other
  conferences before will be accepted only if significant and clear
  enhancements to the tool are reported and implemented.

EXTENDED ABSTRACTS/POSTERS. Submissions, not exceeding two (2) pages,
  briefly introducing work in progress, student work, or preliminary
  results. These papers are expected to be presented as posters at the
  conference.

Further information about paper submission, including a more detailed
description of the scope and specification of the three submission
categories, will be made available at SAT 2012 web page. The review
process will be subject to a rebuttal phase. 

IMPORTANT DATES:
================
  Abstract Submission:			05/02/2012
  Paper Submission:		 	12/02/2012 
  Rebuttal phase:                    28-30/03/2012
  Final Notification:			12/04/2012      
  Final Version Due:			04/05/2012

  SAT/SMT School:                    12-15/06/2012
  Workshops:				16/06/2012
  Conference:                        17-20/06/2012

PROCEEDINGS
===========

The proceedings of SAT 2012 will be published by Springer-Verlag in the
LNCS series. 

PROGRAM CHAIRS
==============

Alessandro Cimatti -- FBK-Irst, Trento, Italy
Roberto Sebastiani -- DISI, University of Trento, Italy

PROGRAM COMMITTEE 
=================

Dimitris Achlioptas -- UC Santa Cruz, USA
Fahiem Bacchus -- University of Toronto, Canada
Paul Beame -- University of Washington, USA
Armin Biere -- Johannes Kepler University, Austria
Randal Bryant -- Carnegie Mellon University, USA
Uwe Bubeck -- University of Paderborn, Germany
Nadia Creignou -- Aix-Marseille Université, France
Leonardo DeMoura -- Microsoft Research, USA
John Franco -- University of Cincinnati, USA
Malay Ganai -- NEC, USA
Enrico Giunchiglia -- Università di Genova, Italy
Youssef Hamadi -- Microsoft Research, UK
Zyiad Hanna -- Jasper, USA
Holger Hoos -- University of British Columbia, Canada
Marijn Heule -- Johannes Kepler University, Austria
Kazuo Iwama -- Kyoto University, Japan
Oliver Kullmann -- Swansea University, UK
Daniel Le Berre -- Université d’Artois, France
Ines Lynce -- Instituto Superior Técnico, Portugal
Panagiotis Manolios -- Northeastern University, USA
Joao Marques-Silva -- University College Dublin, Ireland
David Mitchell -- Simon Fraser University, Canada
Alexander Nadel -- Intel, Israel
Jussi Rintanen -- The Austrailan National University, Australia
Lakhdar Sais -- Université d’Artois, France
Karem Sakallah -- University of Michigan, USA
Bart Selman -- Cornell University, USA
Laurent Simon -- Université Paris 11, France
Carsten Sinz -- Karlsruhe Institute of Technology, Germany
Niklas Sorensson -- Chalmers University, Sweden
Ofer Strichman -- Technion, Israel
Stefan Szeider -- Vienna University of Technology, Austria
Allen Van Gelder -- University of California, Santa Cruz, USA
Toby Walsh -- University of New South Wales, Australia
Xishun Zhao -- Sun Yat-Sen University, China