the heuristic replies with [<span style="font-variant:small-caps;">\#AddClause($\{\bot\}$)</span>]{} causing the termination of the CDCL returning [<span style="font-variant:small-caps;">inconsistent</span>]{}; otherwise, [<span style="font-variant:small-caps;">\#fallback($0, \emptyset, \emptyset, \emptyset$)</span>]{} is sent to go on with the default heuristic.

\[ex:rintanen\] In [@DBLP:journals/ai/Rintanen12], a heuristic for solving the planning problem modeled as SAT problem is proposed that intuitively forces the solver to prefer short and simple plans. This criterion can be implemented in our framework by using the event [<span style="font-variant:small-caps;">OnSearch($\Gamma',\A$)</span>]{}, and the request [<span style="font-variant:small-caps;">GetChoice</span>($I$)]{}. In fact, [<span style="font-variant:small-caps;">OnSearch(.)</span>]{} allows the driver to identify *actions* and *goals* literals; while the answer to [<span style="font-variant:small-caps;">GetChoice</span>(.)]{} is computed by running the algorithm in Figure 3 of [@DBLP:journals/ai/Rintanen12].

We mention that, one can easily obtain all the [<span style="font-variant:small-caps;">vsids</span>]{}-like heuristics described in [@DBLP:conf/sat/BiereF15] by applying small modifications to the solution presented in Example \[ex:minisat\].

Case study: Answer Set Programming
==================================

In this section we report on a case study that provides pragmatical evidence of the applicability of our framework. The case study is developed in the context of Answer Set Programming (ASP) [@DBLP:journals/cacm/BrewkaET11]. ASP is a declarative problem solving paradigm proposed in the area of logic programming and non-monotonic reasoning. ASP is an ideal test bed for our framework for two main 