Date: 07-May-2008 Title: SAT Race 2008 solvers descriptions available! Hits: 54 Contributed by: Daniel Le Berre Keywords: SAT tools, SAT-Solver Competition, null         Carsten Sinz just made available the descriptions of the solvers participating to the SAT Race 2008. Some submissions are particularily interesting: there is one ASP solver (CLASP), one SMT solver driver (Barcelogic) and the successor of Oepir (KW). The winners will be announced next week (on May 15) during the SAT Conference.

Date: 06-May-2008 Title: HWMCC'08 Call for Model Checkers and Benchmarks Hits: 20 Contributed by: Armin Biere Keywords: Verification, EDA, Benchmark, SAT application, SAT tools         In case you have not noticed, in 2008 there is a new incarnation of the hardware model checking competition (HWMCC'08). If you have benchmarks in BLIF, SMV, VERILOG, or even AIGER, please consider to submit them to the competition. We are also looking for fair cycle respectively liveness properties this time. And last but not least prepare your model checker to be submitted as well.. In particular, note the qualification round deadline at the end of this month (May 30). Final submission deadline is June 13.

Date: 04-May-2008 Title: SymCon'08: Eighth International Workshop on Symmetry in Constraint Satisfaction Problems Hits: 24 Contributed by: Daniel Le Berre Keywords:         To be held at CP 2008, Sidney, Australia, September 15th 2008 WORKSHOP DESCRIPTION SymCon'08 is the 8th in a series of workshops affiliated with the CP conference, and focuses on the investigation of symmetry and symmetry breaking techniques for Constraint Satisfaction Problems (CSPs). Symmetries occur frequently in CSPs. When undetected, they cause thrashing during traditional backtracking search by redundantly exploring symmetric parts of the search space. The topic was discussed as far back as 1874 by Glaisher, and new techniques to detect and/or break symmetry have been proposed in recent years. However, many outstanding problems remain. For instance, the detection and exploitation of local, dynamic, and weak forms of symmetry remains a challenge. The workshop is a forum for researchers to present advances in symmetry breaking techniques and to discuss the above or other open problems. Additionally, the workshop welcomes the presentation of applications and case studies that exhibit some form of symmetry. The workshop is relevant to the computational group theory (CGT) community because CGT is often the theory underlying many symmetry breaking techniques. Importantly, the organizers welcome submissions from researchers working in other areas of Artificial Intelligence who feel that their work would be of interest to the CP community. Such areas include planning, model checking, QBF formulas, finite model search, and theorem proving in FOL. Workshop topics include, but are not limited to: - Symmetry definition: semantic symmetry, syntactic symmetry, constraint symmetry, solution symmetry - Automatic symmetry detection: static approaches and dynamic approaches - Global symmetry detection and elimination - Dynamic symmetry detection and elimination - Combining symmetry breaking techniques - Exploiting weak forms of symmetries like "dominance" and "almost-symmetries" - Case studies of problems that exhibit interesting symmetries - Application of computational group theory techniques to symmetry breaking - Heuristics that use information about symmetry to guide search - Elimination and avoidance of symmetry by re-modelling - Dynamic avoidance of symmetric states during search - Complexity analysis of symmetry breaking techniques - Application of CSPs to symmetry and related algebraic problems - Comparing symmetry breaking techniques in constraint programming with techniques for dealing with symmetry in other search domains - Symmetry in CNF formulas and OBF formulas - Symmetry in finite model search in first order logic - Novel exploitation of symmetry in varied search domains of interest to the CP community IMPORTANT DATES Submission deadline: Sunday, 29th June 2008 Notification of acceptance: Thursday, 17th July 2008 Camera ready deadline: Sunday, 3rd August 2008 Workshop: Monday, 15th September 2008 PROGRAM COMMITTEE CHAIRS - Fadi Aloul American University of Sharjah, UAE Email: faloul@aus.edu - Belaid Benhamou University of Provence (Aix-Marseille I) LSIS-CMI, 39 F. Joliot-Curie 13453 Marseille Cedex13 France. Email: Belaid.Benhamou@cmi.univ-mrs.fr - Lakhdar Sais University of Artois Rue Jean Souvraz SP-18 F-62307 Lens Cedex 3, France E-mail : sais@cril.fr

Date: 02-May-2008 Title: QiCP'08: Second International Workshop on Quantification in Constraint Programming Hits: 20 Contributed by: Daniel Le Berre Keywords: QBF, CSP, call for papers         held in conjunction with CP'2008, Sydney, Australia, Sept 14, 2008. Overview: Constraint Programming is a very successful paradigm to express combinatoral problems for which it provides both a representation language and powerful solving techniques. Modeling uncertainty in data and/or the presence of an adversary can be done by introducing universally quantified and/or stochastic variables. They are used to encode possible alternative that have to be all taken into account to provide a robust solution. Possible applications are games, robust scheduling, conformant planning or model checking for the discrete case. For continuous variables, it includes control design, verification of safety and performance conditions of a system in engineering or determination of values of design variables compatible with all values of some uncertain physical data. The first workshop on Quantification in Constraint Programming has been held in conjuction with CP'2005 in Sitges, Spain. Since then, there has been an increasing attention to this topic in the areas of QBF, QCSP and continuous constraints. The aim of this workshop is to collect papers describing novel and ongoing works in the field, and to foster discussions and cross-fertilization between different approaches. Scope: This workshop is open to all aspects related to quantification in Constraint Programming and SAT. The aim of the workshop is to present ongoing work and to exchange ideas on modeling and solving quantified problems. Topics that may be addressed in papers for consideration for inclusion in this workshop include, but are not limited to: - Search and propagation algorithm - Modeling issues with quantified languages - Complexity results - Quantified global constraints - Quantified languages design and compilation - Strategy extraction and representation - Over-constrained quantified problems, explanations - First-order constraints - Quantification in CHR - Uncertainty handling - Stochastic constraint programming - Implementation issues - Other types of variables, non-backtrackable variables where domain prunings are not undone on backtracking - Applications and benchmarks of Quantified Constraints, QBF and Stochastic CSP Submissions: The workshop is open to all members of the CP community. Submitted papers can be up to 15 pages in length, describing work on one or more of the topics relevant to the workshop. Alternatively, a shorter paper (maximum 5 pages) can be submitted, presenting a research statement or perspective on topics relevant to the workshop. All submissions will be reviewed and accepted papers will be published in the workshop proceedings. At least one author must attend the workshop. The proceedings will be available electronically on the workshop web page and in hardcopy at CP 2008. We encourage authors to submit papers electronically in pdf format. Papers should be formatted using the Lecture Notes in Computer Science (LNCS) style. All submissions should include the author's name(s), affiliation, complete mailing address, and email address. Workshop papers will be published in workshop notes as well as on the Web. Please send your submission by email to the workshop organizers, using the subject line "QiCP'2008 submission": enrico@dist.unige.it, arnaud.lallouet@univ-orleans.fr, rueher@essi.fr Important Dates: Paper submission : July 11, 2008 Notification : July 30, 2008 Final version : August 20, 2008 Organizing Committee: Enrico Giunchiglia, University of Genova, Italy. Arnaud Lallouet, University of Orléans, France. Michel Rueher, University of Nice, France.

Date: 02-May-2008 Title: First Workshop on Counting Problems in CSP and SAT, and other neighbouring problems, Counting'08 Hits: 32 Contributed by: Daniel Le Berre Keywords: null         Held in conjunction with the 14th International Conference on Principles and Practice of Constraint Programming, CP'08, Sidney Technical Description The problems of counting the number of models in a SAT instance, or counting the number of solutions in CSPs belong to the class of #P-complete problems, introduced by Leslie Valiant in 1979. It's computational complexity can be therefore considered as extreme, either in theory or in practice. Nevertheless, this problem can be considered as fundamental in areas such as statistics, statistical physics or artificial intelligence with applications in the analysis of probabilistic systems (in genetics, computer vision...). Moreover, the interest of the community on Counting Problems in CSP and SAT, and other related problems has increased in the last years. The recent works on this subject are not just theoretical and have began to produce solvers capable of solving non trivial instances. Several classes of approaches have been proposed, considering exact counting, bounds on the number of models (or solutions), dedicated to specific classes of constraints... These results have frequently been obtained by extending results proposed by the CP (or SAT) community. This workshop would like to bring together researchers interested in all aspects of counting problems, such as: - complexity results - tractability - theoretical frameworks - solving algorithms - exact methods - approximation and bounds - problem modeling - applications of counting to other problems - integration of weights and probabilities - combining/integrating different frameworks and algorithms - comparative studies - real-life applications Workshop Format Its aim is to provide a forum where researchers currently working in this area can discuss their most recent ideas and developments and think together about the most promising new directions, and also about applications where this problem is crucial. Therefore we will encourage the presentation of work in progress or on specialized aspects of counting problems and also on real-life applications. One day workshop Paper Submission Paper submissions should contain original material and must not exceed 15 pages. Submissions should use the Springer LNCS style. All appendices, tables, figures and the bibliography must fit into the page limit. Submissions deviating from these requirements may be rejected without review. Submit papers (PDF files) to the following email addresses: philippe.jegou@univ-cezanne.fr Thomas.Schiex@spam-remove.toulouse.inra.fr selman@cs.cornell.edu Important dates Paper Submission June 23 Notification July 25 Final Versions August 20 Workshop Date September 14 Workshop Organizers - Philippe Jegou, Universite Paul Cezanne, France (contact information) - Thomas Schiex, INRA, France - Bart Selman, Cornell University, USA Program Committee Fahiem Bacchus, University of Toronto Nadia Creignou, Universite de la Mediterranee, Marseille, France Rina Dechter, University of California, Irvine, USA Arnaud Durand, Universite Denit Diderot, Paris, France Carla Gomes, Cornell University, USA Philippe Jegou, Universite Paul Cezanne, Marseille, France Samba-Ndojh Ndiaye, Universite Paul Cezanne, Marseille, France Gilles Pesant, Université de Montréal, Canada Ashish Sabharwal, Cornell University, USA Thomas Schiex, INRA, France Bart Selman, Cornell University, USA

Date: 29-Apr-2008 Title: Search in ManyCore 1.0 Hits: 36 Contributed by: Daniel Le Berre Keywords: Alternative approach, Distributed Computing, distributed parallel dynamic learning         In conjunction with, International Conference on Principles and Practice of Constraint Programming (CP'08), International Conference on Automated Planning and Scheduling (ICAPS'08), International Conference on Knowledge Representation and Reasoning(KR'08), 12th International Workshop on Non-monotonic Reasoning (NMR'08) . September 15, 2008. Sydney, Australia. Organizers Youssef Hamadi and Pascal Van Hentenryck. Workshop description Recent years have shown a major architectural shift in computer hardware. The traditional efficiency gains upcoming from the relentless raise of chips frequencies has been stopped by a thermal wall and performance improvements have to be found elsewhere. The new direction is to add more computing units (cores) to a chip in order to raise its computational power. The products resulting from this multi-core strategy are now on every desktop and yet the horizon is wide open since the number of cores is expected to grow exponentially. The previous technological shift represents an important challenge for many computer sciences fields whose best algorithms have to be rethought for manycore-based parallelization. The goal of this workshop is to provide a forum which will consider the consequences of the previous shift for constraint-based combinatorial search. The scope is not restricted to constraint programming or constraint satisfaction, and the organizers would particularly welcome contributions related to Automated Planning or to any other related domain. In order to encourage the systematic and principled exploration of manycore based parallel search, this event will welcome works on all the aspects of parallel search. Typical topics include, but are not restricted to: · Parallel search · Hybrid parallel search · Knowledge sharing in search · Determinism in parallel search Attendance At least one author of each accepted submission must attend the workshop. Presentation and submission format Half-day workshop. Full papers of no more than 15 pages formatted using the LNCS style, http://www.springer.de/comp/lncs/authors.html. Short papers (at least 3 pages or 3,000 words) addressing an important problem for further research or describing an interesting lesson learned. Papers must be addressed in pdf to youssefh at microsoft dot com. Important dates Submission deadline: June 23th Notification of acceptance: July 28th Camera-ready copy deadline: August 4th Workshop: September 15th Program committee · Tanj Bennett, Microsoft, Redmond, USA · Youssef Hamadi, Microsoft Research , Cambridge, UK · Pascal Van Hentenryck, Brown University, Brown, USA · Simon Kasif, Boston University, Boston, USA · Richard Korf, UCLA, Los Angeles, USA · Vipin Kumar, University of Minnesota, Minneapolis, USA · Bertrand Mazure, CRIL-CNRS, Lens, France · Yehuda Naveh, IBM Research, Haifa, Israel · Lakhdar Sais, CRIL-CNRS, Lens, France · Tobias Schubert, Albert-Ludwigs-University of Freiburg, Freiburg, Germany Contact information Youssef Hamadi. Email: youssefh at microsoft dot com

Date: 29-Apr-2008 Title: SofT'08 - 9th Workshop on Preferences and Soft Constraints Hits: 37 Contributed by: Joao Marques-Silva Keywords: CSP, MAXSAT, SoftSAT, null         9th Workshop on Preferences and Soft Constraints, SofT'08 Special year on Cost Function Processing Held in conjunction with the 14th International Conference on Principles and Practice of Constraint Programming, CP'08 http://soft08.ecs.soton.ac.uk Technical Description --------------------- Preferences are ubiquitous in real life: most problems are over-constrained and would not be solvable if we insist that all their requirements are strictly met. Moreover, many problems are more naturally described via preference rather than hard statements. Soft constraints are the way the constraint community has extended its classical framework to deal with the concept of preferences. This workshop will bring together researchers interested in all aspects of soft constraints and cost function processing, such as: - theoretical frameworks - problem modeling - solving algorithms - languages - preference aggregation and elicitation - multi-objective or qualitative optimization - combining/integrating different frameworks and algorithms - comparative studies - real-life applications This year, the workshop is more specifically oriented towards the various algorithmic aspects of discrete cost function processing, which is a very general problem related to preference and soft constraint processing. The workshop is an opportunity to share knowledge between people working around algorithms and solvers for formalisms, including Weighted Max-SAT, Soft CSP, Bayesian Networks, Random Markov Field, Factor Graphs, Pseudo Boolean Optimization, SAT Modulo Theories, and related formalisms. Workshop Format --------------- This workshop is intended to build on the experience and success of the CP'99 to CP'06 workshops on the same subject and the recent meeting on cost function processing (25 attendees during two days). Its aim is to provide a forum where researchers currently working in this area can discuss their most recent ideas and developments and think together about the most promising new directions. Therefore, we encourage the presentation of work in progress or on specialized aspects of preferences, soft constraints, and more generally, cost function processing. Papers that bridge the gap between theory and practice are especially welcome. Paper Submission ---------------- Paper submissions should contain original material and must not exceed 15 pages. Submissions should use the Springer LNCS style. All appendices, tables, figures and the bibliography must fit into the page limit. Submissions deviating from these requirements may be rejected without review. Submit papers to the following email addresses: degivry@toulouse.inra.fr jpms@ecs.soton.ac.uk pedro@iiia.csic.es Important dates ---------------- Paper Submission June 23 Notification July 25 Final Versions August 20 Workshop Date September 15 Workshop Organizers -------------------- Simon de Givry, INRA, Toulouse, France Joao Marques-Silva, University of Southampton, UK Pedro Meseguer, CSIC, Barcelona, Spain Program Committee --------------------- Hachemi Bennaceur, CRIL, France Rina Dechter, University of California, Irvine, USA Hector Geffner, Universitat Pompeu Fabra, Spain Simon de Givry, INRA, France Jimmy H. M. Lee, Chinese University of Hong Kong, China Joao Marques-Silva, University of Southampton, UK Felip Manya, CSIC, Spain Pedro Meseguer, CSIC, Spain Francesca Rossi, University of Padova, Italy Marti Sanchez, INRA, France Thomas Schiex, INRA, France Toby Walsh, National ICT, Australia

Date: 23-Apr-2008 Title: Doctoral Student Positions Available Hits: 50 Contributed by: Marco Roveri Keywords: Job         Doctoral Student Positions Available Design and Verification of Embedded Software Embedded System Research Unit Fondazione Bruno Kessler (formerly part of IRST - Centro per la Ricerca Scientifica e Tecnologica) Trento, Italy Deadlines: May 31, 2008 The Embedded System Research Unit (http://es.fbk.eu) of the Bruno Kessler Foundation, Trento, Italy, is seeking several candidates for Ph.D positions. The Ph.D. studies will be held at the International Doctorate School in Information and Communication Technologies (http://www.ict.unitn.it/) of the University of Trento, Italy. The research activity will be carried out within the Embedded Systems Unit of the Center for Scientific and Technological Research of the Fondazione Bruno Kessler. The research activity will aim at techniques, methodologies and support tools for the design and verification of embedded systems. In particular, possible topics will include: - Embedded Software Design and Verification - Formal Requirements Analysis - Design and Verification of Hybrid and Timed systems The selected candidates will be initially enrolled in a stage and, if they pass the selection of the Ph.D. school, they will be enrolled as Ph.D. students. Ph.D. courses will start in Autumn 2008, and the thesis must be completed in three or four years. People enrolled in a stage and subsequent Ph.D. courses are expected to move to Trento, and will receive monetary support during both phases of their activity. Candidate Profile ================= The ideal candidate should have an MS or equivalent degree in computer science, mathematics or electronic engineering, and combine solid theoretical background and software development skills. The candidate should be able to work in a collaborative environment, with a strong commitment to reaching research excellence and achieving assigned objectives. Background knowledge and/or previous experience in the following areas, though not mandatory, will be considered favorably: - Symbolic Model Checking, - Propositional Satisfiability, - Satisfiability Modulo Theory, - Constraint Solving and Optimization, - Formal Requirements Analysis, - Software Verification, - Software Synthesis, - Embedded System Design Languages (e.g. Verilog, VHDL, System C, and System Verilog), - Safety Analysis (FTA, FMEA). Applications and Inquiries ========================== Interested candidates should inquire for further information and/or apply by sending email to jobs[at]fbk[dot]eu. Applications should contain a statement of interest, with a Curriculum Vitae, and three reference persons. PDF format is strongly encouraged. Emails will be automatically processed and should have 'RIF: ES/phd' as subject. Contact Person ============== * Alessandro Cimatti mailto: cimatti[at]fbk[dot]eu http://es.fbk.eu/people/cimatti

Date: 23-Apr-2008 Title: Post-Doc Positions Available Hits: 45 Contributed by: Marco Roveri Keywords: Job         Post-Doc Positions Available Design and Verification of Embedded Software Embedded System Research Unit Fondazione Bruno Kessler (formerly part of IRST - Centro per la Ricerca Scientifica e Tecnologica) Trento, Italy Deadlines: May 31, 2008 The Embedded System Research Unit (http://es.fbk.eu) of the Bruno Kessler Foundation, Trento, Italy, is seeking several candidates for Post-Doc positions. The activities will target algorithms, methodologies and tools for the design and verification of Embedded Systems. The activities will mainly focus on the following topics: - Safety Analysis with focus on Dynamic Fault Tree Analysis - Formal Requirements Analysis - Verification of Hybrid Systems - Verification of SystemC TLM models - Optimization of Design and Installation of Aircraft Architectures The activities will be carried out within two European Projects of the 7th framework, scheduled to start in 2008: - MISSA (http://es.fbk.eu/index.php?n=Projects.MISSA) and - COCONUT (http://es.fbk.eu/index.php?n=Projects.COCONUT). The successful candidates will be enrolled with a fixed length contract (2 to 3 years), and will be subject to a 6 months trial work period. Candidate Profile ================= The ideal candidate should have a Ph.D degree in computer science, mathematics or electronic engineering or proved equivalent experience, combine solid theoretical background and software development skills, and have some degree of autonomy. The candidate should be able to work in a collaborative environment, with a strong commitment to reaching research excellence and achieving assigned objectives. In depth previous experience in at least one of the following areas is required: - Symbolic Model Checking, - Propositional Satisfiability, - Satisfiability Modulo Theory, - Constraint Solving and Optimization, - Formal Requirements Analysis, - Software Verification, - Software Synthesis, - Embedded System Design Languages (e.g. Verilog, VHDL, System C, and System Verilog), - Safety Analysis (FTA, FMEA). Applications and Inquiries ========================== Interested candidates should inquire for further information and/or apply by sending email to jobs[at]fbk[dot]eu. Applications should contain a statement of interest, with a Curriculum Vitae, and three reference persons. PDF format is strongly encouraged. Emails will be automatically processed and should have 'RIF: ES/postdoc' as subject. Contact Person ============== * Alessandro Cimatti mailto: cimatti[at]fbk[dot]eu http://es.fbk.eu/people/cimatti

Date: 23-Apr-2008 Title: PhD / PostDoc Position Opening at the University of Karlsruhe Hits: 75 Contributed by: Daniel Le Berre Keywords: New research position         PhD / PostDoc Position Opening The research group "Verification meets Algorithm Engineering" at the University of Karlsruhe is offering a PhD/PostDoc position in the area of SAT Solving. The focus of this position is on algorithm development for parallel SAT solvers as well as both theoretical and practical work on structured SAT instances. Applicants should have a solid theoretical background in formal methods or mathematical logic, as well as outstanding programming skills. Interest in applications of SAT solving (e.g., product configuration, software verification, or bio-informatics) is also appreciated. The position is initially available for up to three years (with a possible extension) and is open immediately. For additional information or to apply for this position please send an e-mail to sinz@ira.uka.de. Carsten Sinz Institute for Theoretical Computer Science TU Karlsruhe