by considering the needs of well-known heuristics, as well as by applying the lessons learned while developing domain-specific heuristics in the case study reported in the next section.

In our framework we identify two main actors: the *solver* and the *driver*. The first is, basically, an implementation of the CDCL algorithm, and the second implements an external branching heuristic.

Selection of a branching literal may depend (or not depend) on properties of the input, on the (current) solver state, on employed optimization techniques (e.g., input rewritings), as well as on the status of variables that directly model some properties of the problem, etc. This information is possibly communicated by the solver to the driver by means of *events*. Events can be seen as asynchronous messages sent to the driver when specific points of the computation are reached, as detailed in Table \[tab:events\]. The driver could exploit this information to implement the heuristic criteria, e.g., updating counters or modifying its status. None of the events are mandatory for the driver (we expect that an efficient implementation smartly sends only those required by the driver).

We have also identified two main moments in the computation when the solver gets directions from the 