driver. These are modeled in our framework by means of *requests*, that are detailed in Table \[tab:responses\] together with the *responses* the solver expects to receive. Requests are synchronous, i.e., the solver waits for a response of (i.e., a command from) the driver.

The request [<span style="font-variant:small-caps;">GetAtomsToBeFrozen</span>($\A$)]{} is sent before starting the simplifications of the input formula. In fact, preprocessing can remove atoms that the heuristic strategy may want to keep (they may play a role in a domain-specific heuristic). The response [<span style="font-variant:small-caps;">\#Freeze($A \subseteq \A$)</span>]{} informs the solver to avoid eliminating the variables in $\A$.

[|p[.9]{}|]{}\
\
\
*Asks the heuristic strategy to provide a list of atoms $A \subseteq \A$ that must not be removed by simplifications.*\
\

[|p|]{}\
\
*Asks to not remove atoms in $A$ during preprocessing.*\

\
\
\
*Asks the heuristic strategy to provide the next branching literal(s) given the current interpretation $I$.*\
\

[|p|]{}\
\
*Asks the solver to perform the choices in list $\L$. $\L$ contains tuples of the form ($at,sign$), where $at \in \A'$ and $sign \in \{p,n,f\}$. Given tuple $(at,sign)$, the solver chooses $at$ if $sign=p$, $\neg at$ if $sign=n$, and if $sign=f$ the CDCL is left free to choose 