Call for Papers

Cfp as txt-file

Cfp as pdf-file

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.

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 submission pages.


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

  • 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.


SAT'12 is co-located with the Second International SAT/SMT Summer School (June 12-15).
SAT'12 will also host related events like workshops (June 16) and various competitive events.

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, can be found at the submission pages for the three categories. The review process will be subject to a rebuttal phase.

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
Conference: 17-20/06/2012

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

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

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 -- LIF Marseille, 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 -- University of Wales Swansea, 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


cfp.txt6.76 KB
SAT2012-cfp.pdf57.94 KB