Just-in-Time Hierarchical Constraint Decomposition

AAAI Conferences

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.


Circuit Complexity and Decompositions of Global Constraints

AAAI Conferences

We show that tools from circuit complexity can be used to study decompositions of global constraints. In particular, we study decompositions of global constraints into conjunctive normal form with the property that unit propagation on the decomposition enforces the same level of consistency as a specialized propagation algorithm. We prove that a constraint propagator has a a polynomial size decomposition if and only if it can be computed by a polynomial size monotone Boolean circuit. Lower bounds on the size of monotone Boolean circuits thus translate to lower bounds on the size of decompositions of global constraints. For instance, we prove that there is no polynomial sized decomposition of the domain consistency propagator for the alldiff constraint.


Circuit Complexity and Decompositions of Global Constraints

arXiv.org Artificial Intelligence

We show that tools from circuit complexity can be used to study decompositions of global constraints. In particular, we study decompositions of global constraints into conjunctive normal form with the property that unit propagation on the decomposition enforces the same level of consistency as a specialized propagation algorithm. We prove that a constraint propagator has a a polynomial size decomposition if and only if it can be computed by a polynomial size monotone Boolean circuit. Lower bounds on the size of monotone Boolean circuits thus translate to lower bounds on the size of decompositions of global constraints. For instance, we prove that there is no polynomial sized decomposition of the domain consistency propagator for the ALLDIFFERENT constraint.


Translation-Based Constraint Answer Set Solving

AAAI Conferences

We solve constraint satisfaction problems through translation to answer set programming (ASP). Our reformulations have the property that unit-propagation in the ASP solver achieves well defined local consistency properties like arc, bound and range consistency. Experiments demonstrate the computational value of this approach.


Translation-based Constraint Answer Set Solving

arXiv.org Artificial Intelligence

We solve constraint satisfaction problems through translation to answer set programming (ASP). Our reformulations have the property that unit-propagation in the ASP solver achieves well defined local consistency properties like arc, bound and range consistency. Experiments demonstrate the computational value of this approach.