Date: 24-Jan-2012 Title: Announcement / Call for Participation SAT Challenge 2012 Hits: 29 Contributed by: Daniel Le Berre Keywords: General Interest         ----- SAT Challenge 2012 ----- Affiliated with SAT 2012, June 17-20, Trento, Italy The SAT Challenge 2012 is a competitive event for solvers for the Boolean Satisfiability (SAT) problem. It is organized as a satellite event to the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012) and stands in the tradition of the SAT Competitions that have been held yearly from 2002 to 2005 and biannually starting from 2007, and the SAT-Races held in 2006, 2008 and 2010. The area of SAT solving has seen tremendous progress over the last years. Many problems (e.g., in hardware and software verification) that seemed to be completely out of reach a decade ago can now be handled routinely. Besides new algorithms and better heuristics, refined implementation techniques turned out to be vital for this success. To keep up the driving force in improving SAT solvers, we want to motivate implementors to present their work to a broader audience and to compare it with that of others. THE CHALLENGE The SAT Challenge differs from both previous SAT Competitions and SAT-Races. Similar to SAT Competitions, there will be several tracks suitable for different kinds of solving algorithms (e.g. complete or local search). Similar to SAT-Races, the time to solve each instance will be limited to 15 minutes, and the solvers' source code need not be made publicly available (although this is strongly encouraged). The SAT Challenge 2012 will consist of 6 independent tracks, including: * Four Main Tracks for Sequential Solvers: - Application SAT+UNSAT: problem encodings (both SAT and UNSAT) from real-world applications. - Hard Combinatorial SAT+UNSAT: hard combinatorial problems (both SAT and UNSAT) to challenge current SAT solving algorithms. - Random SAT: randomly generated satisfiable instances. - Random UNSAT: randomly generated unsatisfiable instances. * Parallel Solver Track: Same problem instances as in the Application Main Track. Four cores of a CPU can be used. * Sequential Portfolio Solver Track: Same problem instances as in the Application Main Track. A portfolio solver combines different SAT algorithms. IMPORTANT DATES March 11, 2012: Deadline for registering solvers. March 26, 2012: Deadline for handing in benchmarks. March 26, 2012: Test runs of solvers finished, begin of feedback/revision period. April 11, 2012: Deadline for submitting final versions of solvers. Around June 20, 2012: Announcement of results at the SAT 2012 conference. ORGANIZING COMMITTEE Adrian Balint University of Ulm, Germany Anton Belov University College Dublin, Ireland Matti Jarvisalo University of Helsinki, Finland Carsten Sinz Karlsruhe Institute of Technology, Germany

Date: 23-Jan-2012 Title: Opening of the Vienna Center for Logic and Algorithms (VCLA) January 25-26, 2012 Hits: 11 Contributed by: Stefan Szeider Keywords: null         [apologies if you receive multiple copies of this message] The Vienna Center for Logic and Algorithms (www.VCLA.at) is an initiative of Vienna University of Technology (TU Vienna). Located at the Faculty of Informatics, the Center promotes international scientific collaboration in logic and algorithms. The Center celebrates its opening through the following three events: SYMPOSIUM "LOGIC AND ALGORITHMS: A SCIENTIFIC PERSPECTIVE" Wednesday, 25th January 2012, 9:00-15:00, Festsaal, TU Vienna Invited Speakers: * Edmund M. Clarke, Carnegie Mellon University * Fedor V. Fomin, University of Bergen * Thomas A. Henzinger, IST Austria * Joao Marques-Silva, University College Dublin & IST/INESC-ID * Georg Weissenbacher, Princeton University OFFICIAL OPENING CEREMONY Wednesday, 25th January 2012, 15:00-16:00, Festsaal, TU Vienna Speakers: * Sabine Seidler, Rector of the TU Vienna * Gerald Steinhardt, Dean of the Faculty of Informatics, TU Vienna * Stefan Szeider and Helmut Veith, VCLA, Co-chairs, TU Vienna AWARD OF A HONORARY DOCTORATE TO E.M. CLARKE Thursday, 26th January 2012, 10:00, Boecklsaal, TU Vienna For details see the Center's website at http://www.VCLA.at

Date: 17-Jan-2012 Title: Research Scientist/Programming Position Available SDG/CSAIL@MIT Hits: 14 Contributed by: Daniel Le Berre Keywords: Job         The Software Design Group in MIT’s Computer Science and Artificial Intelligence Lab (CSAIL) is hiring a Research Scientist to participate in research and development of the Alloy language and analyzer. Alloy (http://alloy.mit.edu) is a lightweight modeling language with an automatic analyzer based on SAT. It has been used in a wide range of applications in software engineering, including the design of access control schemes, security mechanisms, network protocols, ontologies, and so on. In addition to design analysis, Alloy has also been used for code verification, test case generation and automatic configuration. Alloy was introduced in 1997, and is now in version 4. Hundreds of papers have been written describing research based on Alloy; for examples, see http://alloy.mit.edu/applications.html. Alloy has also been taught in dozens of university courses. Our plan now is to take Alloy in new directions, and dramatically improve the usability and scalability of the analyzer. We are looking for someone who is is excited by these possibilities and will be deeply involved not only in design and implementation but also in strategic planning. There are also opportunities to co-advise students and participate in research proposals. Qualifications should include: a PhD in computer science or a related field; superb programming skills, preferably with experience of writing compiler-like tools; familiarity with logic and model checking; a passion for design; excellent communication and writing skills; ability to work both independently and cooperatively with others. Please apply online to MIT (http://jobs.mit.edu/) with resume and cover letter, and include the following in your application (sent separately to djresci@csail.mit.edu): (A) A list of languages and technologies you're familiar with; (B) A short sample of something you've written in English, and a small code sample; (C) A short answer to the question: "If you could make one big change to the Alloy system, what would it be?" Please reference MIT job number 00008292 in your application.

Date: 11-Jan-2012 Title: Call for Papers - IWSBP 2012 Hits: 37 Contributed by: Miroslav Velev Keywords: Repository, Verification, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Instance simplification, Satisfiable Problems Generation, SAT tools, call for papers, null, null         Call for Papers - IWSBP 2012 ------------------------------------------------------------------------- Please, feel free to forward this message to interested people. We apologize if you receive this email more than once. ------------------------------------------------------------------------- Dear colleague, the 10th International Workshop on Boolean Problems will be held on September 19-21, 2012, in Freiberg, Germany. More information you can find on the workshop web page http://www.informatik.tu-freiberg.de/prof2/ws_bp10/ Deadlines Submission - May 5, 2012 Acceptance notices - June 9, 2012 Final version submission - July 7, 2012 Sincerely, Prof. Dr.-Ing. habil. Bernd Steinbach Call for Papers The workshop on Boolean problems has an emphasis on the problems related to the solution of all kinds of high-dimension Boolean and discrete problems, and provides a forum for researchers and engineers from different disciplines to exchange ideas. The workshop is devoted to theoretical discoveries as well as practical applications. An aim of the workshop is to initiate possible collaborative research and to find new areas of application. It is intended to publish the papers in proceedings. The invited speakers - Mitch Thornton (SMU Dallas (Texas), USA), - Raimund Ubar (TTU Tallinn, Estonia), and - Vincent Gaudet (University of Waterloo, Canada) are presenting essential results of their research. Topics of interest (not limited to) Theory Properties and applications of Boolean Algebras Data Structures and Algorithms Modeling Specification of data structures/algorithms Complexity Program Systems/Software Fundamental software for the solution of Boolean Problems Comparison of efficiency Practical Applications Application of Boolean algebra in FPGA synthesis Quantum logic, reversible logic, and multi-valued logic Solution of real-world problems Submissions To submit a paper, please send an extended abstract, no longer than 6 pages, as a PDF file to iwsbp2012@informatik.tu-freiberg.de or using the workshop web page http://www.informatik.tu-freiberg.de/prof2/ws_bp10/ by April 25, 2012. Acceptance notices will be sent by June 9, 2012. The final version of the paper should be submitted by July 7, 2012. Program Committee - J. Butler, Naval Postgraduate School Monterey, USA - R. Berghammer, C-A-University of Kiel, Germany - L. Cheremisinova, Minsk Academy of Science, Belarus - D. Debnath, Oakland University, USA - R. Drechsler, University of Bremen, Germany - E. Dubrova, Royal Institute of Technology (KTH), Sweden - G. Dueck, University of New Brunswick, Canada - D. Große , University of Bremen, Germany - I. Levin, Tel Aviv University, Israel - T. Luba, Warsaw University of Technology, Poland - M. Miller, University of Victoria, Canada - C. Moraga, TU Dortmund, Germany - M. A. Perkowski, Portland State University, USA - Y. Pottosin, Minsk Academy of Science, Belarus - T. Sasao, Kyushu Institute of Technology, Japan - Ch. Scholl, University of Freiburg, Germany - R. Stankovic, University of Nis, Serbia - B. Steinbach, University of Freiberg, Germany - R. Ubar, Tallinn Technical University, Estonia - M. Velev, Aries Design Automation, USA - A. De Vos, University of Gent, Belgium - S. Yanushkevich, University of Calgary, Canada - A. D. Zakrewskij, Minsk Academy of Science, Belarus Conference Language: English Conference Location: Freiberg University of Mining and Technology, Freiberg (Sachs.), Germany

Date: 05-Jan-2012 Title: CPAIOR 2012 workshop call Hits: 34 Contributed by: Thierry Petit Keywords: CSP         CPAIOR 2012 - CALL FOR WORKSHOP PROPOSAL Ninth International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming, Cité des Congrès, Nantes, France, May 28 - June 1, 2012. http://www.emn.fr/z-info/cpaior-2012/ The CPAIOR 2012 conference chairs invite proposals for the workshop program. CPAIOR 2012 workshops will provide an informal setting where workshop participants will have the opportunity to discuss specific technical topics in an atmosphere that facilitates the active exchange of ideas. It is an opportunity to disseminate work in progress or to promote new and emerging areas on the intersection of CP, AI, and OR. All workshops will take place on May 29, 2012, at the site of the main conference. Workshops can be proposed for a full or a half day. The internal format of the workshop will be determined by the organizers of each workshop. Proposals for workshops should contain the following information: - The title and a brief technical description of the workshop, specifying the goals and the technical issues it will focus on (this description is meant to be published on the main conference homepage). - The intended duration of the workshop (full/half day). - A brief discussion of why and to whom the workshop is of interest. - A list of related workshops held within the last three years, if any, and their relation to the proposed workshop. - The names of the proposed organizing committee. - The name and email address of the main organizer. Each workshop main organizer will be responsible for: - Creating a web site for the workshop that will be linked from the CPAIOR 2012 website. - Organizing the technical program: call for papers, selecting submissions, inviting attendant, etc.  - Providing working pdf notes to be duplicated for the workshop by May 11, 2012. The CPAIOR 2012 conference chairs will be responsible for the following: - Providing publicity for the workshop series as a whole. - Providing logistics support and a meeting place for the workshop. - Scheduling workshops in cooperation with the workshop organizers. - Duplicating working notes (possibly in electronic form) and distributing them to the participants. All proposals should be submitted by electronic mail (in ASCII), to the workshop chair. Important Dates: February 6, 2012: Proposal submission deadline. February 13, 2012: Acceptance notification. February 27, 2012: Deadline for receipt of the URL and Call for Papers/Participation for the workshop.  May 11, 2012: Deadline for workshop working notes. May 29, 2010: CPAIOR 2012 workshops. CPAIOR 2012 Workshop Chair: Thierry Petit, Co-Head TASC, LINA / Ecole des Mines de Nantes. Thierry.Petit@mines-nantes.fr

Date: 20-Dec-2011 Title: Learning and Intelligent OptimizatioN Conference LION 6, Paris, Jan 16-20, 2012 Hits: 225 Contributed by: Daniel Le Berre Keywords: MAXSAT         The conference is dedicated to various forms of optimization. As such, there is a session related to MAXSAT. See the technical program for details.

Date: 19-Dec-2011 Title: Second International SAT/SMT Summer School Hits: 49 Contributed by: Marco Roveri Keywords: null, null         Second International SAT/SMT Summer School Trento, Italy, June 12-15th, 2012 http://satsmtschool2012.fbk.eu The SAT/SMT Summer School 2012 (2nd edition) aims at providing graduate students and researchers from universities and industry with a comprehensive overview of the research in SAT, SMT, and their application. The lectures cover the foundational and practical aspects of SAT and SMT solvers, as well as their application to verification, planning, scheduling, and optimization problems. This second edition follows the Summer School of 2011 organized by Vijay Ganesh at MIT, and is co-located with the SAT 2012 conference. The school will take place in Trento, Italy, from June 12th to June 15th 2012. The program will feature four lectures per day, with the first two days dedicated to SAT and SMT foundations, and the last two to applications on various domains. List of speakers: Armin Biere (Johannes Kepler University, Linz, Austria) Leonardo de Moura (Microsoft Research Redmond, USA) Bruno Dutertre (SRI International, USA) Martin Fränzle (Carl von Ossietzky Universität Oldenburg, Germany) John Franco (University of Cincinnati, USA) Silvio Ghilardi (Università di Milano, Italy) Patrice Godefroid (Microsoft Research Redmond, USA) Holger Hoos (University of British Columbia, Vancouver, Canada) Tomi Janhunen (Aalto University, Finland) Pete Manolios (Northeastern University, USA) Joao Marques-Silva (University College Dublin, Ireland) Ken McMillan (Microsoft Research Redmond, USA) Jussi Rintanen (Austrialian National University, Australia) Fabio Somenzi (University of Colorado, Boulder, USA) Gunnar Stålmarck (Prover Technology and Gain Sweden AB, Sweden) Cesare Tinelli (University of Iowa, USA) A more detailed program is available at the school website (http://satsmtschool2012.fbk.eu). It is expected that we will be able to provide a limited number of grants for students that will attend the school. More details about the procedure for applying and the registration deadlines will appear on the school website as soon as possible. Interested students are however encouraged to contact us at any moment. The school organizers, Alberto Griggio <griggio@fbk.eu> and Stefano Tonetta <tonettas@fbk.eu>

Date: 30-Nov-2011 Title: Atrenta Research Position Hits: 68 Contributed by: Scott Cotton Keywords: Verification, EDA, SAT application, SAT tools, SAT Hardware, Satisfiability Modulo Theory         --------------------------------------------------------------------------- [[[ We apologize if you receive multiple copies of this message ]]] --------------------------------------------------------------------------- Job Description: ================= The research activity will aim at investigating and developing novel techniques, methodologies and support tools for the verification of circuit designs in particular the use of Satisfiability Modulo Theories (SMT), however researcher with background on other verification techniques are also encouraged to apply. Candidate Profile: ================= World class researcher in EE/CS/Math (particularly formal theory), familiar with predicate logic, temporal logic (e.g., CTL, LTL), model checking, familiar with complexity of algorithms, very strong in algorithm development -- including design and implementation of large programs, very strong in mathematical considerations in the development of CAD tools/EDA and familiarity with design practice. Intimate knowledge of solvers such as BDD, SAT, ATPG, SMT and symbolic simulation algorithms. Capability of working with prospective customers. Experience in a Semiconductor company is helpful but not absolutely essential. Job Requirements: ================= BS in EE/CS/Math. with 9+ years of relevant experience, MS with 7+ years of relevant experience, or related Ph.D. It is essential that the individual has strong desires to learn and explore new technologies and are able to demonstrate good analysis and problem solving skills. Prior knowledge and experience of CAD tool/EDA development are a big plus. Job site: ========= The researcher will be part of Atrenta's EU based advanced research center and can work from any EU country. The company will not sponsor immigration visa. Contact Person ============== Fahim@atrenta.com

Date: 26-Nov-2011 Title: CALL FOR WORKSHOP PROPOSALS Hits: 62 Contributed by: Daniel Le Berre Keywords: General Interest         ------------------------------------------------------------------------- 15th International Conference on THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT'12 Trento, Italy, June 17-20th, 2012 http://sat2012.fbk.eu/ CALL FOR WORKSHOP PROPOSALS ------------------------------------------------------------------------- CALL FOR SAT'12-ASSOCIATED WORKSHOPS PROPOSALS Researchers and practitioners are invited to submit proposals for associated workshops on topics related to the SAT conference. The workshops will be held in parallel the day before the conference (June 16th 2011), immediatly after the SAT/SMT school. See http://sat2012.fbk.eu. Proposals should consist of two parts. * a short scientific justification of the proposed topic, its significance, and the particular benefits of the workshop to the community, as well as a list of previous or related workshops (if relevant). * an organizational part should include contact information of the workshop organizers, procedures for selecting papers and participants, estimate of the audience size and a tentative list of the program committee. Proposals are due by 20.12.2012 and must be submitted by email to both SAT'12 Conference Chairs: cimatti@fbk.eu and rseba@disi.unitn.it. If you are interested in proposing a workshop, or you're considering doing that, please contact us in advence. Alessandro Cimatti and Roberto Sebastiani SAT2012 Chairs

Date: 23-Nov-2011 Title: Atrenta Job Opportunity Hits: 131 Contributed by: Scott Cotton Keywords: SAT application, SAT tools, SAT-Based, SAT Hardware, Satisfiability Modulo Theory, null         World class researcher in EE/CS/Math (particularly formal theory), familiar with predicate logic, temporal logic (e.g., CTL, LTL), model checking, familiar with complexity of algorithms, very strong in algorithm development -- including design and implementation of large programs, very strong in mathematical considerations in the development of CAD tools/EDA and familiarity with design practice. Intimate knowledge and familiarity with one of this techniques BDD, SAT, SMT, ATPG and symbolic simulation algorithms. Capability of working with prospective customers. Experience in a Semiconductor company is helpful but not absolutely essential. Job Requirements: BS in EE/CS/Math. with 9+ years of relevant experience, MS with 7+ years of relevant experience, or related Ph.D. It is essential that the individual has strong desires to learn and explore new technologies and are able to demonstrate good analysis and problem solving skills. Prior knowledge and experience of CAD tool/EDA development is a definite plus.