SAT & CP


Making the link between SAT and CP is a very important research topic. The two approaches have very orthogonal views and assets, however, they are very close in many algorithmic aspects.

My first paper was on encoding CSPs into CNF such that a given level of consistency is achieved by unit propagation.

Moreover, I have recently started to work on the topic of clause learning in the context of constraint programming. In particular, in the context of his Ph.D. Thesis, Mohamed Siala developed a version of the solver Mistral that do conflict directed clause learning even for some global constraints.

Publications on SAT Encodings and Hybrid Systems



Recently, we were surprised to see that, during the CSP solver competitions, a very simple model in Mistral was actually very efficient on some job shop and open shop instances. Starting from this observation, we came to the conclusion that techniques that are very commonly used in SAT, such as restarting whilst using an adaptive heuristic or a very simple form of nogood learning were the main reasons for this surprising results. Together with Diarmuid Grimes, we published a number of papers on this topic.
Also, here are the slides of the master class on this topic that I gave at CPAIOR 2011.

Publications on SAT-based Methods for Scheduling