the default heuristic.

-   [$\textsc{Quick{PUP\xspace}}^*$]{}is a modification of [<span style="font-variant:small-caps;">Quick[PUP]{}</span>]{}that tests already used units first and a new one afterwards.

-   [<span style="font-variant:small-caps;">Pred</span>]{} [@DBLP:conf/ictai/Drescher12] tries first to connect an unassigned zone or sensor to one of the units that already have connections to neighbour zones or sensors, i.e. reachable over at most two input zone-sensor relations. If this fails, [<span style="font-variant:small-caps;">Pred</span>]{}tries a new unit first and used ones subsequently.

#### Implementation details.

We implemented the four heuristics in [<span style="font-variant:small-caps;">wasp</span>]{}using the C++ interface given in Section \[sec:heur\]. A heuristic is initialized as [<span style="font-variant:small-caps;">OnSearch($\Gamma',\A'$)</span>]{} event is invoked by the solver. Next, the ordering of vertices is generated and used to determine sets of chosen literals $L$ in response to [<span style="font-variant:small-caps;">GetChoice</span>($I$)]{} requests. In addition, a heuristic registers [<span style="font-variant:small-caps;">OnUnrollLit($\ell$)</span>]{} events in order to synchronize its inner state with decisions made by [<span style="font-variant:small-caps;">wasp</span>]{}between two subsequent [<span style="font-variant:small-caps;">GetChoice</span>($I$)]{} requests. If a heuristic finds that the current partial interpretation is inconsistent, i.e. no further assignments can be made, it backtracks and sends [<span style="font-variant:small-caps;">\#Unroll($\ell$)</span>]{} to [<span style="font-variant:small-caps;">wasp</span>]{}. In this case, $\ell$ is one of the literals that were selected by a heuristic at the previous choice event. Finally, the fallback from [<span 