Date: 15-May-2013 Title: Third International SAT/SMT Summer School Hits: 10 Contributed by: Tomi Janhunen Keywords: null         SECOND CALL FOR PARTICIPATION Third International SAT/SMT Summer School Aalto University, Otaniemi Campus Espoo, Finland, July 3-5th, 2013 http://satsmt2013.ics.aalto.fi/ REGISTRATION: The registration deadline for the school is May 20, 2013. Full details of the registration procedure are available at the school website (http://satsmt2013.ics.aalto.fi/). ABOUT: The SAT/SMT Summer School aims at providing graduate students and researchers from universities and industry with a comprehensive overview of research and methodology in satisfiability testing (SAT) and satisfiability modulo theories (SMT). The lectures cover the foundational and practical aspects of SAT and SMT technologies and their applications. The third edition follows the schools that took place at MIT (SAT/SMT Solver Summer School 2011) and at Fondazione Bruno Kessler (SAT/SMT School 2012) in Trento, Italy. The 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013) is arranged at University of Helsinki the following week (see http://sat2013.cs.helsinki.fi/). The program will feature four lectures per day, with the first two days dedicated to SAT and SMT, and the last to special topics. Two of the lectures will be organized as tutorials giving hands-on experience on SAT/SMT-based modelling. List of invited lectures: Proof Complexity by Olaf Beyersdorff, University of Leeds, United Kingdom Applications of SMT Solvers by Alessandro Cimatti, IRST, Trento, Italy Internals of Modern SMT Solvers by Leonardo de Moura, Microsoft Research, Redmond, USA Foundations and Theoretical Aspects of SAT by John Franco, University of Cincinnati, USA SAT-Based Planning by Enrico Giunchiglia, University of Genoa, Italy Preprocessing by Marijn Heule, University of Texas at Austin, USA CDCL SAT Solvers and SAT-Based Problem Solving by Joao Marques-Silva, University College Dublin, Ireland SMT Theory and DPLL(T) by Albert Oliveras, Technical University of Catalonia, Barcelona, Spain Modelling and Solving in Answer Set Programming by Torsten Schaub, Potsdam University, Germany Parametrized Complexity by Stefan Szeider, Vienna University of Technology, Austria A more detailed program is available at the school website (http://satsmt2013.ics.aalto.fi/). Organizing committee: Keijo Heljanko, Aalto University, Tomi Janhunen, Aalto University, and Matti Jarvisalo, University of Helsinki.

Date: 04-May-2013 Title: SAT 2013 Preliminary program Hits: 33 Contributed by: Matti Järvisalo Keywords: null         SAT 2013 Preliminary Conference Program 16th International Conference on Theory and Applications of Satisfiability Testing July 8-12, 2013, Helsinki, Finland Registration (early registration deadline May 27) http://sat2013.cs.helsinki.fi/registration.html Program updates: http://sat2013.cs.helsinki.fi/program.html ----------------------------------------------------------------------------- MONDAY July 8 9:00-17:00: Workshops SMT 2013: 11th International Workshop on Satisfiability Modulo Theories PoS 2013: 4th International Workshop on Pragmatics of SAT Breaks: 10:30-11:00 Coffee 12:30-14:00 Lunch 15:00-15:30 Coffee -------------- TUESDAY July 9 9:00-12:30: Workshops SMT 2013: 11th International Workshop on Satisfiability Modulo Theories QBF 2013: International Workshop on Quantified Boolean Formulas 12:30-14:00 Lunch (only to participants with a full conference registration) 14:00-14:20 Welcome, best paper announcement 14:20-15:20 Invited talk: Albert Atserias "The Proof-Search Problem between Bounded-Width Resolution and Bounded-Degree Semi-Algebraic Proofs" 15:20-15:50 Coffee 15:50-16:50 Propositional Proof Complexity I -Exponential Separations in a Hierarchy of Clause Learning Proof Systems -The Complexity of Theorem Proving in Autoepistemic Logic Social program: Welcome Reception ----------------- WEDNESDAY July 10 9:00-10:30 Quantified Boolean Formulas -On Propositional QBF Expansions and Q-Resolution -Recovering and Utilizing Partial Duality in QBF -Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation 10:30-11:00 Coffee 11:00-12:30 Parallel Solving -Soundness of Inprocessing in Clause Sharing SAT Solvers -Concurrent Clause Strengthening -Parallel MUS Extraction 12:20-14:00 Lunch 14:00-15:00 Invited talk: Edmund M. Clarke "Turing's Computable Real Numbers and Why They Are Still Important Today" 15:00-15:30 Coffee 15:30-16:50 Maximum Satisfiability -A Modular Approach to MaxSAT Modulo Theories -Exploiting the Power of MIPs Solvers in Maxsat -Community-based Partitioning for MaxSAT Solving General Assembly of the SAT Association (open to all conference participants) ---------------- THURSDAY July 11 9:00-10:30 Encodings and Applications -Experiments with Reduction Finding -A Constraint Satisfaction Approach for Programmable Logic Detailed Placement -Minimizing Models for Tseitin-Encoded SAT Instances 10:30-11:00 Coffee 11:00-12:30 Beyond SAT -Solutions for Hard and Soft Constraints Using Optimized Probabilistic Satisfiability -Quantified Maximum Satisfiability: A Core-Guided Approach -Nested Boolean Functions as Models for Quantified Boolean Formulas 12:30-14:00 Lunch 14:00-15:00 Invited talk: Peter Stuckey "There Are No CNF Problems" 15:00-15:30 Coffee 15:30-16:50 Solver Techniques and Analysis -Factoring Out Assumptions to Speed Up MUS Extraction -On the Interpolation between Product-Based Message Passing Heuristics for SAT -Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction Social Program: Conference Banquet -------------- FRIDAY July 12 9:00-9:30 Tool paper presentations 9:30-10:30 Competition Overviews 10:30-11:30 Combined tool demo and poster session, coffee 11:30-12:30 Clique-Width and SAT -A SAT Approach to Clique-Width -Cliquewidth and Knowledge Compilation 12:30-14:00 Lunch 14:00-15:00 Propositional Proof Complexity II -A Rank Lower Bound for Cutting Planes Proofs of Ramsey's Theorem -On the Resolution Complexity of Graph Non-Isomorphism *** Note: no break here *** 15:00-15:50 Parameterized Complexity -Local Backbones -Upper and Lower Bounds for Weak Backdoor Set Detection 15:50: Closing Ceremony, Drinks

Date: 02-May-2013 Title: SAT 2013 Call for Participation Hits: 64 Contributed by: Matti Järvisalo Keywords: null         [ We apologize if you receive multiple copies of this call. ] ------------------------------------------------------------------------- CALL FOR PARTICIPATION Sixteenth International Conference on THEORY AND APPLICATIONS OF SATISFIABILITY TESTING --- SAT 2013 --- Helsinki, Finland, July 8-12, 2013 http://sat2013.cs.helsinki.fi/ Registration to SAT 2013 is now open at http://sat2013.cs.helsinki.fi/registration.html Early registration deadline: May 27, 2013 ------------------------------------------------------------------------- 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 at http://sat2013.cs.helsinki.fi/accepted.html -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 VENUE ============== SAT 2013 takes place in Helsinki, the capital of Finland, a vibrant scandinavian and international city that is easily access from various destinations within Europe and around the world. SAT 2013 is organized at University of Helsinki in the very heart of the city. SAT 2013 takes place during the main summer season, allowing one to experience the whitenights during which the sun almost never sets.

Date: 30-Apr-2013 Title: QBF 2013: Second Deadline Extension Hits: 39 Contributed by: Anonymous Keywords:         The submission deadline for QBF 2013 has been extended a second time. The new deadline is: *** Wednesday, May 8 23:59 (anywhere on Earth) *** QBF 2013 (workshop at SAT 2013): http://fmv.jku.at/qbf2013/

Date: 26-Apr-2013 Title: SAT 2013 Call for Posters Hits: 55 Contributed by: Matti Järvisalo Keywords: null         ------------------------------------------------------------------------- CALL FOR PRESENTATION-ONLY POSTERS Sixteenth International Conference on THEORY AND APPLICATIONS OF SATISFIABILITY TESTING --- SAT 2013 --- Helsinki, Finland, July 8-12, 2013 http://sat2013.cs.helsinki.fi/ *** Acceptance notifications are sent within one week of submission *** Poster abstract submissions by : May 17, 2013 Notifications by : May 22, 2013 Conference early registration deadline : May 27, 2013 ------------------------------------------------------------------------- The SAT 2013 conference invites submissions of 200-400 word poster abstracts. Each submitted abstract will be checked for suitability for presentation as a poster during a poster-session at the main conference. The poster abstracts may be about (but not restricted to): -SAT-related work-in-progress. -SAT-related work recently published or accepted for publication at other major conferences, workshops, or journals. -Descriptions of SAT-related systems, interesting benchmark problems, etc. -Overviews of SAT-related PhD theses or currently on-going PhD work. -Overviews of SAT-related research projects. To submit a poster abstract, send the title, list of authors and their affiliations, and a 200-400 word abstract of your poster by email to sat2013@easychair.org . The submissions should be in ASCII text. The accepted poster abstracts will not appear in the SAT 2013 proceedings, but will be included in the informal conference booklet made available to all registered attendees. Each poster presenter is expected to register to the main conference. SAT 2013 includes three high-quality invited talks (by Albert Atserias, Edmund M. Clarke, and Peter Stuckey), around 30 scientific presentations, various satellite events including the SMT, PoS, and QBF workshops and competition reports, as well as a lively social program.

Date: 24-Apr-2013 Title: QBF 2013: Deadline Extension Hits: 52 Contributed by: Anonymous Keywords:         The QBF 2013 paper submission deadline is extended to *** Sunday, April 28 23:59 (anywhere on Earth) *** QBF 2013 (workshop at SAT 2013): http://fmv.jku.at/qbf2013/

Date: 19-Apr-2013 Title: Raman-Charpak Fellowship Hits: 62 Contributed by: Ateet Bhalla Keywords: General Interest         Department of Science and Technology (DST), Government of India and the French Embassy in India, Ministry of Foreign Affairs, Government of France, Indo French Centre for Promotion of Advanced Research (IFCPAR/CEFIPRA) invites applications from the PhD students of India and France for awarding the Raman-Charpak Fellowship 2013. The programme aims at developing and strengthening Indo-French scientific cooperation through close collaboration between Indian and French laboratories, by supporting the mobility of highly qualified PhD students registered in an Indian or French research institute/ university, to offer them an excellent opportunity for carrying out a part of their doctoral research work in France / India. Deadline for application submission: May 31' 2013 contact:bhalla.ateet@gmail.com

Date: 17-Apr-2013 Title: Pragmatics of SAT 2013: slight deadline extension Hits: 86 Contributed by: Daniel Le Berre Keywords: General Interest         The fourth Pragmatics of SAT workshop submission deadlines have been slightly extended: abstracts will be accepted until April 20, and papers until April 24.

Date: 17-Apr-2013 Title: Configurable SAT Solver Challenge (CSSC) 2013 Hits: 79 Contributed by: Daniel Le Berre Keywords: General Interest         CALL FOR CONTRIBUTIONS Configurable SAT Solver Challenge (CSSC) 2013 http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/ Event affiliated with SAT 2013 Conference http://sat2013.cs.helsinki.fi/ 8-12 July 2013, Helsinki, Finland ----------------------- Most modern SAT solvers have many parameters that can be altered to adjust their behavior and performance. This year, we are introducing the first Configurable SAT Solver Challenge (CSSC), a competitive event that assesses the *peak performance* of such parametric solvers (i.e., performance with optimized parameters). CSSC recognizes that the value of a SAT solver for a given application is often due to the performance achieved after customization for that application rather than merely the performance of its default configuration. To obtain a good approximation of the peak performance attainable in practice, we will use a fixed computational budget to optimize parameter settings with each of several different state-of-the-art software packages (so-called algorithm configuration procedures). We will reward SAT solvers that can be flexibly configured to perform well in different circumstances (as opposed to having one single best configuration). The results will be presented at this year's SAT conference (8-12 July in Helsinki, Finland). We invite submissions of both configurable SAT solvers and benchmark instance generators. Although we will accept proprietary solvers, only open-source submissions will be eligible for prizes. To minimize the overhead for solver designers, the deadlines are arranged to fall just after those of the SAT competition. More details about the submission process and the rules of the competition can be found on the CSSC 2013 website at http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/ ===== Important Dates ===== 30 April 2013: Solver and benchmark registration opens 1 June 2013: final submission of solvers and benchmarks 9-12 July 2013: presentation of results during SAT 2013 Conference ===== Organizers ===== Frank Hutter (Freiburg University) Adrian Balint (Ulm University) Sam Bayless (University of British Columbia) Holger Hoos (University of British Columbia) Kevin Leyton-Brown (University of British Columbia) ===== Contact ===== cssc.organizers@gmail.com http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013

Date: 17-Apr-2013 Title: QBF 2013: Second Call For Papers Hits: 64 Contributed by: Anonymous Keywords:         [We apologize if you receive multiple copies of this call] ------------------------------------------------------------------------ CALL FOR PAPERS QBF 2013 International Workshop on Quantified Boolean Formulas Helsinki, Finland, July 9, 2013 http://fmv.jku.at/qbf2013/ Affiliated to and co-located with: SAT 2013 conference Helsinki, Finland, July 8-12, 2013 http://sat2013.cs.helsinki.fi/ ------------------------------------------------------------------------ The goal of the International Workshop on Quantified Boolean Formulas (QBF 2013) is to bring together researchers working on theoretical and practical aspects of QBF solving. In addition to that, it addresses (potential) users of QBF in order to reflect on the state-of-the-art and to consolidate on immediate and long-term research challenges. The workshop also targets researchers working with quantifiers in other formalisms like Constraint Satisfaction Problems (CSP) and Satisfiability Modulo Theories (SMT) in order to exchange experiences and ideas. =============== IMPORTANT DATES =============== Please follow http://fmv.jku.at/qbf2013/ for any updates. April 24 2013: paper submission May 20 2013: notification of acceptance June 15 2013: camera-ready version of papers July 9 2013: workshop ================== TOPICS OF INTEREST ================== The workshop is concerned with all aspects of current research on QBF and related formalisms with quantifiers. The topics of interest include (but are not limited to): - QBF applications, encodings and benchmarks - Case studies and experimental evaluations - Certificates and proofs for QBF - Formats of proofs and certificates - Implementations of proof checkers and verifiers - Decision procedures for QBF - Calculi for QBF - Data structures, implementation details and heuristics - Pre- and inprocessing techniques - Structural QBF solving - Quantifiers in other formalisms like SMT or CSP - Tools related to any aspect of QBF/CSP/SMT reasoning ================================ SUBMISSION OF EXTENDED ABSTRACTS ================================ Submitted extended abstracts should have an overall length of 4 pages in LNCS format excluding references. Authors may decide to include an appendix with additional material. Appendices will be considered at the reviewers' discretion. Please see the submission website for further guidelines: http://fmv.jku.at/qbf2013/submission.html =============== WORKSHOP REPORT =============== Accepted extended abstracts are collected in an informal report which will be publicly available at the workshop's website. ============== PROGRAM CHAIRS ============== Florian Lonsing Vienna University of Technology, Austria Martina Seidl Johannes Kepler University Linz, Austria ================= PROGRAM COMMITTEE ================= Fahiem Bacchus Armin Biere Nikolaj Björner Uwe Bubeck Hans Kleine Büning Hubie Chen Nadia Creignou Uwe Egly Allen Van Gelder Enrico Giunchiglia Mikoláš Janota Massimo Narizzano Stefan Szeider