SAT and Hybrid Models of the Car Sequencing Problem

Christian Artigues (1) , Emmanuel Hébrard (1) , Valentin Mayer-Eichberger (2, 3) , Mohamed Siala (1) , Toby Walsh (2, 3)

1 LAAS-ROC - Équipe Recherche Opérationnelle, Optimisation Combinatoire et Contraintes
2 NICTA - National ICT Australia [Sydney]
3 UNSW - University of New South Wales [Sydney]

We compare both pure SAT and hybrid CP/SAT models for solving car sequencing problems, and close 13 out of the 23 large open instances in CSPLib. Three features of these models are crucial to improving the state of the art in this domain. For quickly finding solutions, advanced CP heuristics are important and good propagation (either by a specialized propagator or by a sophisticated SAT encoding that simulates one) is necessary. For proving infeasibility, clause learning in the SAT solver is critical. Our models contain a number of novelties. In our hybrid models, for example, we develop a linear time mechanism for explaining failure and pruning the AtMostSeqCard constraint. In our SAT models, we give powerful encodings for the same constraint. Our research demonstrates the strength and complementarity of SAT and hybrid methods for solving difficult sequencing problems.

Mots clés: Car-Sequencing; SAT; Constraint Programming; Lazy Clause Generation

Domaines: Intelligence artificielle [cs.AI]

Christian Artigues, Emmanuel Hébrard, Valentin Mayer-Eichberger, Mohamed Siala, Toby Walsh. SAT and Hybrid Models of the Car Sequencing Problem. 11th International Conference, CPAIOR 2014, Cork, Ireland, May 19-23, 2014., May 2014, Cork, Ireland. pp.268-283, ⟨10.1007/978-3-319-07046-9_19⟩. ⟨hal-00991036⟩