Association Française pour la Programmation par Contraintes – Programmation par Contraintes: Décrivez votre problème, laissez les solveurs le résoudre Programmation par Contraintes: Décrivez votre problème, laissez les solveurs le résoudre

Postdoc position in Propositional Satisfiability at CRIL University of Artois, Lens (France)

==================================================================

PostDoctoral position proposal in Propositional Satisfiability

==================================================================

Algorithms for Inference and Constraints group (CRIL, CNRS UMR 8188), at Lens (France), is offering a postDoctoral position.

-–

ANR TUPLES wesite: http://www.lsis.org/tuples/

CRIL website: http://www.cril.univ-artois.fr/

Contact:

Web: http://www.cril.univ-artois.fr/~sais/

E-mail: sais@cril.fr

Requirements for a candidate:

• A PhD in Computer Science or equivalent diploma;

• Expertise in Propositional Satisfiability (SAT), constraint programming (CP); Good programming skills.

Offered:

• A full time, temporary appointment for a period of 6 months;

• Starting date: from September 2014 but possibly later (the postdoc has to take place between September 2014 and April 2015);

• Monthly salary: 2000 euros net and negotiable based on the qualification profile;

This postdoc deals with the practical application of tractability results to enhance the efficiency of SAT solvers. Until now, tractable classes have usually been studied from a purely theoretical point of view, their practical use for solving general instances have not received much attention. For example, the current SAT solvers do not perform any tractability analysis before or during the resolution of a given instance.

Our goal in this work is to bridge the gap between theory and practice by effectively exploiting the tractability/intractability results to design the next generation of SAT solvers. The different results obtained in the ANR project TUPLES “Tractability for Understanding and Pushing forward the Limits of Efficient Solvers” will give us several possible research issues for the design of both strong simplification techniques (pre-processing) and efficient solvers.

The consortium has a great experience in the development of SAT solvers. The CRIL team host and maintain several solvers, which have won awards in the different SAT competitions.

Applications should include the following materials:

  • a motivation letter

  • a detailed CV (with publications)

  • two references

Please apply as soon as possible. A first selection will be done during the last week of July 2014. Later applications will be considered if no applicant has been selected at this date.

The position is located at CRIL, University of Artois, Lens (France).

Contact: Lakhdar Sais (sais@cril.fr)


archive

Archive