Conflict-driven constraint answer set solving

Abstract

Constraint answer set programming (CASP) is a declarative problem solving paradigm that combines the strengths of answer set programming (ASP) and constraint programming (CP). ASP solvers provide good computational performance by conflict-driven nogood learning (CDNL) and exploiting unfounded sets. To model features like finite domain variables and global constraints, which are naturally dealt with in CP, hybrid CASP systems have been developed that delegate CP constructs to a CP solver. While this achieved some success, hybrid systems do not seamlessly integrate with CDNL. We address this deficiency by devising two alternative approaches that accommodate CDNL.

For one, we introduce a translation-based approach. The idea is to enhance ASP with CP constructs through translation to ASP. Implemented as preprocessing, this allows us to apply existing CDNL-enabled ASP systems to CASP solving. Our contributions include various generic translations that work for any constraint, and specialised encodings for important global constraints such as ALL-DIFFERENT, GRAMMAR, and REACHABILITY. We show that the inference of ASP solvers can simulate the effect of complex CP algorithms in many cases. Propagation of REACHABILITY, however, can be hindered because ASP systems disregard some consequences from unfounded sets for performance reasons. We tackle this weakness by providing more efficient methods using a reduction to the problem of finding dominators in a flowgraph.

For another, we devise an extension to CDNL-based ASP solving that can integrate CP constructs via lazy nogood generation (LNG). Rather than a-priori translations into ASP, the idea of LNG is to make necessary parts of an encoding explicit on demand and only when new information can be propagated. We introduce external propagators to facilitate LNG and incorporate them into a decision procedure for ASP solving that is centred around CDNL. We then demonstrate how to seamlessly integrate constraint propagation with this framework, resulting in a novel approach to CASP solving.

We have implemented a prototypical CASP system to demonstrate some key principles of our approaches. In 2013, it has successfully participated in a model and solve competition, outperforming hybrid systems.