AAAI Publications, Twenty-Ninth AAAI Conference on Artificial Intelligence

Font Size: 
Just-in-Time Hierarchical Constraint Decomposition
Valentin Mayer-Eichberger

Last modified: 2015-03-04


Lazy Clause Generation (LCG) solvers dominate the current constraint programming competitions. These solvers successfully combine systematic propagation based search, global constraints and conflict clause learning from SAT solving into a hybrid approach. My research project extends the LCG methodology by using a mix of eager and lazy encodings and a richer set of constraint decompositions. Global Constraints exhibit a whole hierarchy of different decomposition into more basic constraints. In our work we want to take advantage of such hierarchies and identify criteria on how constraints could be decomposed before and during search.


SAT and CSP: Modeling/Formulations

Full Text: PDF