a variety of known heuristic criteria from the literature [@DBLP:conf/sat/BiereF15; @DBLP:journals/ai/Rintanen12]. Pragmatic evidence of the benefits of our framework in devising problem-specific heuristics is provided by reporting on a use case where two hard industrial domains defined by Siemens, the Partner Units Problem ([PUP]{}) [@DBLP:conf/iaai/TeppanFF12] and Combined Configuration Problem ([CCP]{}) [@DBLP:conf/lpnmr/GebserRS15], are solved efficiently.

In our use case, the framework has been implemented by extending the ASP solver [<span style="font-variant:small-caps;">wasp</span>]{} [@DBLP:conf/lpnmr/AlvianoDLR15]. Our implementation offers a wide range of possibilities to end users for developing new heuristics. In particular, it offers multi-language support including scripting languages for fast prototyping, an embedded C++ interface for performance-oriented implementations, as well as heuristic definition by means of declarative predicate-based paradigms.

Experiments on [PUP]{}and [CCP]{}confirm the viability of the framework in real-world scenarios, and the effectiveness of our implementation that is able to solve successfully hard problem instances which were not solvable by state-of-the-art ASP solvers. Furthermore, we were able to solve hardest [CCP]{}instances for which no solution was known before.

An overview of the CDCL algorithm
=================================

In this section we provide some basic knowledge about the Conflict-Driven Clause Learning (CDCL) algorithm [@DBLP:journals/tc/Marques-SilvaS99] for solving the satisfiability problem (SAT)  [@DBLP:conf/sat/BiereF15]. The Conflict-Driven Clause Learning 