<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><font class="Apple-style-span" face="Consolas"><span class="Apple-style-span" style="font-size: 14px;"> 15th International Conference on <br> THEORY AND APPLICATIONS OF SATISFIABILITY TESTING <br> --- SAT 2012 ---<br><br> Trento, Italy, June 17-20th, 2012<br> <a href="http://sat2012.fbk.eu/">http://sat2012.fbk.eu/</a><br><br><br>AIM and SCOPE<br>=============<br><br>The International Conference on Theory and Applications of<br>Satisfiability Testing (SAT) is the primary annual meeting for<br>researchers studying the propositional satisfiability<br>problem. Importantly, here SAT is interpreted in a rather broad sense:<br>besides plain propositional satisfiability, it includes the domains of<br>MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean<br>Formulae (QBF), Satisfiability Modulo Theories (SMT), Constraints<br>Programming (CSP) techniques for word-level problems and their<br>propositional encoding.<br><br>To this extent, many hard combinatorial problems can be encoded as SAT<br>instances, in the broad sense mentioned above, including problems that<br>arise in hardware and software verification, AI planning and<br>scheduling, OR resource allocation, etc. The theoretical and practical<br>advances in SAT research over the past twenty years have contributed<br>to making SAT technology an indispensable tool in these domains.<br><br>SAT 2012 will take place in Trento, Italy, a cosmopolitan city set in<br>a spectacular mountain scenery, and home to a world-class university<br>and research centres.<br><br>RELEVANT TOPICS <br>===============<br><br>The topics of the conference span practical and theoretical research<br>on SAT (in the broader sense above) and its applications, and include,<br>but are not limited to: <br><br>* Theoretical issues<br> - Combinatorial Theory of SAT<br> - Proof Systems and Proof Complexity in SAT<br> - Analysis of SAT Algorithms<br>* Solving: <br> - Improvements of current solving procedures<br> - Novel solving procedures, techniques and heuristics<br> - Incremental solving<br>* Beyond solving:<br> - Functionalities (e.g., proofs, unsat-cores, interpolants,...)<br> - Optimization <br>* Applications <br> - SAT techniques for other domains<br> - Novel Problem Encodings<br> - Novel Industrial Applications of SAT<br><br>A more detailed description can be found on the web site.<br><br>INVITED SPEAKERS<br>================<br><br>We are honored to announce the following invited speakers at SAT'12:<br><br>* Aaron Bradley, Boulder, USA. <br> "SAT-based Verification with IC3: Foundations and Demands"<br><br>* Donald Knuth, Stanford, USA.<br> "Satisfiability and The Art of Computer Programming"<br><br>The presence of both speakers has been confirmed, although the titles<br> of the talks may be provisional.<br><br>PAPER SUBMISSION<br>================<br><br>Papers must be edited in LATEX using the LNCS format and<br>be submitted electronically as PDF files via EasyChair. <br>We envisage three categories of submissions:<br><br>REGULAR PAPERS. Submissions, not exceeding fourteen (14) pages, should<br> contain original research, and sufficient detail to assess the<br> merits and relevance of the contribution. For papers reporting<br> experimental results, authors are strongly encouraged to make their<br> data available with their submission. Submissions reporting on case<br> studies in an industrial context are strongly invited, and should<br> describe details, weaknesses and strength in sufficient<br> depth. Simultaneous submission to other conferences with proceedings<br> or submission of material that has already been published elsewhere<br> is not allowed.<br><br>TOOL PRESENTATIONS. Submissions, not exceeding four (4) pages, should<br> describe the implemented tool and its novel features. A<br> demonstration is expected to accompany a tool presentation. Papers<br> describing tools that have already been presented in other<br> conferences before will be accepted only if significant and clear<br> enhancements to the tool are reported and implemented.<br><br>EXTENDED ABSTRACTS/POSTERS. Submissions, not exceeding two (2) pages,<br> briefly introducing work in progress, student work, or preliminary<br> results. These papers are expected to be presented as posters at the<br> conference.<br><br>Further information about paper submission, including a more detailed<br>description of the scope and specification of the three submission<br>categories, will be made available at SAT'12 web page. The review<br>process will be subject to a rebuttal phase. <br><br>IMPORTANT DATES:<br>================<br> Abstract Submission:<span class="Apple-tab-span" style="white-space:pre"> </span> <span class="Apple-tab-span" style="white-space:pre"> </span>05/02/2012<br> Paper Submission:<span class="Apple-tab-span" style="white-space:pre"> </span> <span class="Apple-tab-span" style="white-space:pre"> </span>12/02/2012 <br> Rebuttal phase: 28-30/03/2012<br> Final Notification:<span class="Apple-tab-span" style="white-space:pre"> </span>12/04/2012 <br> Final Version Due:<span class="Apple-tab-span" style="white-space:pre"> </span>04/05/2012<br> Conference: 17-20/06/2012<br><br>PROCEEDINGS<br>===========<br><br>The proceedings of SAT’12 will be published by Springer-Verlag in the<br>LNCS series. <br><br>PROGRAM CHAIRS<br>==============<br><br>Alessandro Cimatti -- FBK-Irst, Trento, Italy<br>Roberto Sebastiani -- DISI, University of Trento, Italy<br><br>PROGRAM COMMITTEE <br>=================<br><br>Dimitris Achlioptas -- UC Santa Cruz, USA<br>Fahiem Bacchus -- University of Toronto, Canada<br>Paul Beame -- University of Washington, USA<br>Armin Biere -- Johannes Kepler University, Austria<br>Randal Bryant -- Carnegie Mellon University, USA<br>Uwe Bubeck -- University of Paderborn, Germany<br>Nadia Creignou -- Aix-Marseille Université, France<br>Leonardo DeMoura -- Microsoft Research, USA<br>John Franco -- University of Cincinnati, USA<br>Malay Ganai -- NEC, USA<br>Enrico Giunchiglia -- Università di Genova, Italy<br>Youssef Hamadi -- Microsoft Research, UK<br>Zyiad Hanna -- Jasper, USA<br>Holger Hoos -- University of British Columbia, Canada<br>Marijn Heule -- Johannes Kepler University, Austria<br>Kazuo Iwama -- Kyoto University, Japan<br>Oliver Kullmann -- University of Wales Swansea, UK<br>Daniel Le Berre -- Université d’Artois, France<br>Ines Lynce -- Instituto Superior Técnico, Portugal<br>Panagiotis Manolios -- Northeastern University, USA<br>Joao Marques-Silva -- University College Dublin, Ireland<br>David Mitchell -- Simon Fraser University, Canada<br>Alexander Nadel -- Intel, Israel<br>Jussi Rintanen -- The Austrailan National University, Australia<br>Lakhdar Sais -- Université d’Artois, France<br>Karem Sakallah -- University of Michigan, USA<br>Bart Selman -- Cornell University, USA<br>Laurent Simon -- Université Paris 11, France<br>Carsten Sinz -- Karlsruhe Institute of Technology, Germany<br>Niklas Sorensson -- Chalmers University, Sweden<br>Ofer Strichman -- Technion, Israel<br>Stefan Szeider -- Vienna University of Technology, Austria<br>Allen Van Gelder -- University of California, Santa Cruz, USA<br>Toby Walsh -- University of New South Wales, Australia<br>Xishun Zhao -- Sun Yat-Sen University, China<br></span></font><br></body></html>