software model checking, planning, equivalence checking, bioinformatics, configuration problems, hardware and software test, software package dependencies, cryptography and more [@DBLP:series/faia/2009-185].

As a matter of fact the performance of a CDCL solver heavily depends on the adoption of heuristics that drive the search for solutions. Among these, the heuristic for the selection of the branching literal (i.e., the criterion determining the literal to be assumed true at a given stage of the computation) can dramatically affect the overall performance of an implementation [@DBLP:series/faia/2009-185]. State-of-the-art CDCL implementations feature very good general purpose heuristics belonging to the family of VSIDS [@DBLP:conf/sat/BiereF15; @DBLP:conf/sat/EenS03; @DBLP:conf/dac/MoskewiczMZZM01]. Since their introduction, VSIDS heuristics proved to be a key ingredient for solving many relevant problems [@DBLP:conf/sat/BiereF15]. Nonetheless, no general heuristic is known to be the best possible choice for all problems [@DBLP:journals/ai/HutterXHL14]. Pioneering work on employing domain-specific heuristics corroborates the validity of that idea. In particular, Beame et al. demonstrated the utility of a domain-specific branching heuristic for solving the pebbling formulas with a CDCL solver [@DBLP:journals/jair/BeameKS04]; and Rintanen proposed to replace the standard VSIDS by a domain-heuristics for efficiently solving planning as satisfiability [@DBLP:journals/ai/Rintanen12]. Moreover, Gerhard Friedrich in his joint invited talk at CP-ICLP 2015 described a number 