paths in the search space that cannot lead to a solution, so it can issue a [<span style="font-variant:small-caps;">Unroll</span>($\ell$)]{} to cause a backtrack up to the last choice made before $\ell$. Moreover, the driver could add some additional domain knowledge modeled by a clause $\varphi$ in the solver by answering [<span style="font-variant:small-caps;">\#AddClause($\varphi$)</span>]{}. Finally, there are cases (see next section) in which it makes sense to blend custom heuristics with the default heuristic, to exploit the strengths of both. To this end the driver can respond [<span style="font-variant:small-caps;">\#Fallback($n,\I,\F,\S$)</span>]{} so to force the solver to use its default heuristic for the next $n$ choices. The parameters of [<span style="font-variant:small-caps;">\#Fallback(.)</span>]{} allow to customize this interaction by (possibly) tuning the activity values and the multiplying factors used by the default heuristic.

In the following we provide a number of examples that show how to encode several well-known conflict-based and domain-specific heuristics. This way the reader can appreciate the generality of our proposal that cover the needs of a wide range of conflict-based heuristics as well as domain-heuristics proposed in the literature. Nevertheless, we remark that our framework can be easily extended by adding new events/requests to fit the needs of future applications.

\[ex:minisat\] We first 