the sign.*\
\
\
*Asks the solver to backtrack until $\ell$ becomes undefined. To trigger a restart set $\ell=\bot$.*\
\
\
*Asks the solver to use the default heuristics for the next $n$ choices. The default heuristic is enable permanently if $n \leq 0$. Parameters $\I, \F, \S$ initialize the default heuristics as follows: $\I: A \rightarrow \mathbb{N}$ provides the initial activity of atoms; $\F: A \rightarrow \mathbb{N}$ associates to atoms an amplifying factor; $\S: A \rightarrow \{p,n\}$ to provide a priority on the sign of literals.*\
\
\
*Asks the solver to add the clause $\varphi$ to the formula.*\

\

The [<span style="font-variant:small-caps;">GetChoice</span>($I$)]{} request is the main one, and is made by the solver when a non-deterministic choice is required. A number of responses are possible besides the obvious one where the driver provides the solver with an ordered list of branching literals to be chosen. The list can hold just one element as in many well-known heuristics, or can provide in one call several choices so to reduce communication overheads in domain-heuristics that may provide at once an entire plan of choices. Alternative responses were inspired by domain-specific criteria. For example, the driver is likely to recognize specific 