Volume 1, Number 0, January 2005

Contents

• news: CP online, CP 2005
• publications: books, PhD theses, online journals, special issues, software
• events: forthcoming conferences and workshops
• career news: Postdoc and PhD jobs at Montpellier, PARC, Namur, NICTA (Melbourne), Vidus (Ipswich), KTH (Stockholm), IRST (Trento)
• reports: Workshop on Graph and Hypergraph Decompostions
• profiles: Lisbon Constraint Programming Group

News

Another initiative supported by the CP organizing committee is a new web portal, CP online. This is designed to be a single place for information about constraint programming. Please visit this site, and add your news, conferences announcements, online resources, etc.

CP-2005 will be held in Sitges (near Barcelona) on October 1st to 5th 2005. The conference will be co-located with ICLP. Pedro Meseguer and Javier Larrosa will be local chairs. Peter van Beek will be the program chair. Michela Milano and Zeynep Kiziltan will chair the Doctoral Programme. Submissions due (approx) May 6th 2005.

CP-2006 will be held in Nantes in 2006. Frederic Benhamou will be the program chair.

Publications

Books:

PhD theses:

Ludovic Langevine, Observation de programmes par contraintes et traces d'exécutions : une sémantique générique et une architecture d'analyse dynamique., Some chapters of this thesis are written in English: the technical chapters, 4, 5, 6, and 7, and the Appendix C. INRIA, France, 2004.

Online journals:

If you are a TPLP author who might recall that the Cambridge University Press has agreed that the accepted versions of the TPLP submissions are posted in the Computing Research Repository (CoRR),

We are happy to inform you that thanks to this provision we now have a free online version of TPLP that also includes all book reviews published in TPLP. This online version can also be reached through the home page of the Association for Logic Programming in Leuven,

We would like to thank Qiu Jiang, a student at the National University of Singapore, for creating the website and adding to CoRR the accepted versions of the `missing' papers. We hope that this small contribution of the logic programming community will inspire others in promoting a free access to scientific literature.

We plan to maintain this free online version of TPLP and appeal to prospective TPLP authors to keep helping us in this endevour.

Krzysztof Apt, Maurice Bruynooghe, and Bart Demoen.

Special issues:

Combining Logical Systems. Special issue of Information and Computation. Guest editors: Alessandro Armando and Christophe Ringeissen. Submission deadline: January 22, 2005.

Journal of Heuristics, Special issue on Preferences and Soft Constraints. Guest editors: S. Bistarelli and F. Rossi. Paper submission deadline: February 27th, 2005. Submissions are to be made electronically, by using the Springer online manuscript submission system of the Journal of Heuristics.

Software:

Events

Career news

Assistant Prof and Prof at Univ. of Montpellier

People interested in these positions must have some basic knowledge of french. In addition, to be allowed to be a candidate next spring, applicants must have received the "qualification" label from the french government. This qualification is a very light procedure, but it has to be done **** before October 19th, **** on the Antares web site.

People who would like more information or help for the qualification procedure should contact Christian Bessiere (bessiere@lirmm.fr).

PostDoc at Palo Alto Research Center (PARC)

We invite applications from candidates with research interests in artificial intelligence or intelligent control. Relevant areas include diagnosis, reasoning under uncertainty, multi-agent and distributed systems, planning and scheduling, constraint reasoning, distributed control, and multi-objective optimization. A PhD or substantial relevant experience is required. For more information, please see here.

A subsidiary of Xerox, PARC offers a multidisciplinary environment for pursuing both basic and applied research. Our funding comes from both corporate sources and government agencies. PARC is an Equal Employment Opportunity company committed to workforce diversity.

TA and PhD at Univ. of Namur

The job is 50% of PhD research. We ask the candidate to state his research interests and propose the plan of a PhD in his application. This plan is just indicative, it will help us to select the PhD supervisor and the real plan. Thus, the topic should match the research interests of one or several of the following academics:

Applicants should have a master degree in computer science. The job starts in Jan 2005 for 6 years. Applicants should ask for an application form from: Service du Personnel des FUNDP, rue de Bruxelles 61, B-5000 Namur (Tel.: +32 81/72 40 42) and return it there filled and with a CV, list of publications and a PhD plan proposal before 15 december 2004.

For more information contact the head of the Programming Department, Pierre Yves Schobbens.

PostDocs at National ICT Australia

Openings withing the Network Information Processing Program. Constraint Programming, Researchers Levels B and D

The Network Information Processing Program of NICTA Victoria Laboratory has a research focus on building a robust, efficient and flexible constraint programming platform. Constraint programming will be used as a technology to tackle combinatorial problems arising in all facets of networks: for example, routing, scheduling, and ad- hoc network generation.

The constraint programming research project will be lead by Professor Mark Wallace and includes Professor Peter Stuckey, Professor Michael Maher, Professor Kim Marriott, Dr Zoltan Somogyi, and Professor Toby Walsh as active participants. The starting point for the project is the existing HAL and Mercury languages developed here in Melbourne. The aim is to build an environment which will dramatically enhance the productivity of applications problem solvers and algorithm developers, and enable us to tackle more complex problems than ever before.

The program is seeking to build a team of constraint programmers to drive this exciting project, and subsequently have four positions available, for one Principal Researcher D (4 year fixed term) and three Researcher B (2 x 2 year fixed term & 1 x 4 year fixed term).

Applications: Please visit NICTA Careers to view the criteria essential to the positions and apply online. Enquiries to peter.stuckey@nicta.com.au. Closing date: 20 January 2005.

Vidus, Ipswich, England

Vidus requires a highly experienced scheduling/optimisation expert to join a small team responsible for the conceptualisation, and down streaming into product, of novel scheduling algorithms and architectures. Vidus, located in Ipswich, England, is the leading company in the area of mobile resource scheduling for telecom and utility environments. The expert will contribute to the delivery of major enhancements to taskforce, the company's core scheduling product.

The candidate should demonstrate expertise in Local Search and Constraint Based Scheduling techniques. The role also requires at least 3 years development experience in Java and/or C++. Experience using UML would also be an advantage.

Our standard terms of employment include performance bonus, stock options - we think it's important that everyone has a stake in the business - pension, private healthcare insurance, life assurance, long term incapacity benefits, personal accident insurance and 25 days holiday (plus public holidays).

If you are interested in applying please mail your CV to: julie.fryatt@vidus.com Further information about the position can be obtained from Bob Laithwaite (bob.laithwaite@vidus.com)

Applicants for the above position must be eligible to work in the UK and CVs from agents will not be considered.

PhD at KTW, Sweden

For more information, please consult here.

Researcher and Programmer Positions at ITC-irst

MathSAT is a decision procedure for logic theories combining boolean propositions with constraints over integer and real variables, and uninterpreted functions. It has been applied in different real-world application domains, ranging from formal verification of infinite state systems (e.g. timed and hybrid systems) to planning with resources, equivalence checking and model checking of RTL hardware designs. The MathSAT family of deciders is based on the extension of a DPLL-like propositional satisfiability procedure, used as an assignment enumerator. MathSAT pioneers a lazy and layered approach, where propositional reasoning is tightly integrated with solvers of increasing expressive power, in such a way that more expensive layers are called less frequently. Formal methods are widely applied as powerful verification and early debugging techniques in the development of complex industrial systems. In particular, formal checking at Register-Transfer Level (RTL) is currently a fundamental step in the design of hardware circuits. Most tools for formal checking, however, work at the boolean level, which is not expressive enough to capture the abstract, high level (e.g., structural, word level) information of RTL designs. Tools for formal checking are thus confronted with problems which are "flattened" down to boolean level so that a predominant part of their computational effort is wasted into brute force reasoning at boolean level. Thus, the checking process would greatly benefit from the ability to represent and exploit higher level informations.

The goal of the ORCHID project (Enhanced Formal Checkers for RTL Circuit Designs) is to investigate enhanced SAT-based techniques for RTL formal checking and to deliver better verification tools for RTL designs. These tools will avoid flattening by working directly at a level of expressivity higher than boolean reasoning, and will be able to analyze larger scale RTL designs. The results of the research will be applicable to the extension of any existing formal checkers based on SAT procedures.

The project is carried on with the external collaboration of the Logic and Validation Technologies, Intel Architecture Group in Haifa, Israel.

The project has open positions for a young researcher and a programmer.

Applications should be sent via email to: mathsat-recruit@itc.it using 'ORCHID: application' as subject, and including a statement of interest and a CV. PostScript, PDF, or plain text formats are encouraged. Please use the above address also for further inquiries.

Young researcher:

The activity of the young researcher will include design and implementation of new algorithms and functionalities, their integration into the MathSAT solver, the preparation of project deliverables. Publication of scientific papers will be a primary objective.

Important research objectives include: improving the efficiency of MathSAT by enriching it with new algorithms; extending the expressivity of MathSAT, with new constructs (including, e.g., bitwise operators and memories); developing new integration algorithms and/or improving current ones; developing and implementing new verification tools using MathSAT as a back-end.

The ideal candidate should have a Ph.D. in either computer science, mathematics, electronic engineering or similar topics, and be able to work in a collaborative environment, with a strong commitment to achieving assigned objectives and reaching research excellence.

Background and/or previous experiences in the areas of formal verification, boolean reasoning, deduction systems, hardware description languages, are desired. Good skills in programming in C/C++ and software developing are also desired.

Programmer:

The activity will include the implementation of new algorithms and functionalities, their integration into the MATHSAT solver, maintenance, and benchmarking.

We encourage the application from young, talented master students who may be interested in pursuing a Ph.D. at the International School on Information and Communication Technologies at the University of Trento.

The ideal candidates must have very good skills in programming in C/C++ and software developing, and be able to work in a collaborative environment, with a strong commitment to achieving assigned objectives. Background knowledge and/or previous experience in the areas of formal verification, boolean reasoning, deduction systems, hardware description languages, though not mandatory, will be considered favourably.

Awards

CP or AI researchers can contact Gene Freuder, e.freuder@4c.ucc.ie for further info. Final D

Reports

The workshop on Graph and Hypergraph Decompostions - Methods and Applications in Computer Science was organized jointly by the Wolfgang Pauli Institute (Austria), Laboratoire GREYC CNRS UMR 6072 (France), and Vienna University of Technology (Austria). The organizing committee -composed of Georg Gottlob, Etienne Grandjean, and Nysret Musliu -invited around 31 researchers from all over the world for a two days and a half programme from December 16 till December 18. The invited researchers came from different research communities such as complexity theory, graph and hypergraph decompositions, constraint satisfaction problems and constraint programming, database, mathematics, etc. This mix of disciplines was also reflected in the talks. In particular, the first session was devoted to Graph and Hypergraph Decompositions and Constraint Satisfaction. Rina Dechter presented her AND/OR paradigm that exploits tree-decomposition in search while Dave Cohen talked about structural decompositions of CSP instances. Stefan Szeider presented his work on Dulmage-Mendelson decompositions and SAT. The other sessions covered areas such as tree and hypertree decompositions, trees/hypergraphs and queries, clique-width and acyclicity, the complexity of directed graphs, geometrical aspects of hypergraphs, and matriods. Overall, the workshop created a nice atmosphere for various researchers from various areas to interact and exchange ideas and the organization was excellent!

Profiles