Theory and Applications of Satisfiability Testing - SAT 2012- 15th International Conference.

This volume contains the papers presented at SAT 2012, 15th International Conference on Theory and Applications of Satisfiability Testing, held on June 16-20th in Trento, Italy. SAT 2012 was co-organized and hosted by Fondazione Bruno Kessler (FBK) and University of Trento (UniTN), Trento, Italy. The SAT series originated in 1996 as a series of workshops, and later developed into 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. 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, solving and advanced functionalities, applications. SAT 2012 hosted two workshops: CSPSAT 2012 (Second International Work- shop on the Cross-Fertilization Between CSP and SAT), and PoS’12 (Third In- ternational Workshop on Pragmatics of SAT), and four competitive events: Max- SAT 2012 (Seventh Max-SAT Evaluation), PB12 (Pseudo-Boolean Competition 2012), QBFEVAL’12 (QBF competition 2012), and SAT Challenge 2012. In SAT 2012 we introduced for the first time the possibility of submitting tool-presentation papers, and of directly submitting poster-presentation papers (2-page abstracts). Overall there were 112 submissions (88 full, 10 tool and 14 poster papers). Each submission was reviewed by at least 3 Program Committee members; for the fist time for SAT, the review process involved also a rebuttal phase. The committee decided to accept 52 papers (29 full, 7 tool and 16 poster papers). Notice that 7 full papers were accepted as posters. The program included also two remarkable invited talks: – Aaron Bradley from University of Colorado at Boulder, presented “Under- standing IC3”; – Donald Knuth from Stanford University presented “Satisfiability and The Art of Computer Programming”. Given the interest of the scientific community outside SAT for the work of Donald Knuth, his talk was open to non-SAT’12 attendees, and included also a question- answering session on general topics in Computer Science. SAT 2012 was co-located with the Second International SAT/SMT Summer School, with a program over four days that hosted sixteen speakers. The school gave the opportunity to many students to attend SAT 2012.