consider the [<span style="font-variant:small-caps;">minisat</span>]{}heuristic as described in [@DBLP:conf/sat/EenS03]. This criterion can be implemented in our framework by exploiting the events [<span style="font-variant:small-caps;">OnStartSearch($\Gamma',\A'$)</span>]{} and [<span style="font-variant:small-caps;">OnLearnClause($\varphi$)</span>]{}, as well as the [<span style="font-variant:small-caps;">GetChoice</span>($I$)]{} request. The first is used to initialize the activity values of atoms in the input; the second causes an increment the activity of atoms in the learned clause $\varphi$. Finally, the request [<span style="font-variant:small-caps;">GetChoice</span>($I$)]{} is answered with [<span style="font-variant:small-caps;">\#Choice($\{(a,n)\}$)</span>]{} by the driver, where $a$ is the undefined atom in $I$ with the highest value of activity.

\[ex:pigeonhole\] Consider the famous pigeonhole problem: given $n$ pigeons and $m$ holes, assign each pigeon to exactly one hole in such a way that two different pigeons do not share the same hole. It can be verified that state-of-the-art SAT solvers are not able to solve this problem efficiently when $n > m$, despite it is known that no solution exists in that case. A domain-specific heuristic based on this observation only uses the requests and no event. To [<span style="font-variant:small-caps;">GetAtomsToBeFrozen</span>($\A$)]{} the driver answers to not remove any atom (providing [<span style="font-variant:small-caps;">\#Freeze($\A$)</span>]{}), and computes $n$ and $m$ by interpreting the atoms in $\A$. Once the first choice is requested, if $n > m$ 