  CDCL-based SAT solvers have transformed the field of automated reasoning
owing to their demonstrated efficiency at handling problems arising from
diverse domains. The success of CDCL solvers is owed to the design of clever
heuristics that enable the tight coupling of different components. One of the
core components is phase selection, wherein the solver, during branching,
decides the polarity of the branch to be explored for a given variable. Most of
the state-of-the-art CDCL SAT solvers employ phase-saving as a phase selection
heuristic, which was proposed to address the potential inefficiencies arising
from far-backtracking. In light of the emergence of chronological backtracking
in CDCL solvers, we re-examine the efficiency of phase saving. Our empirical
evaluation leads to a surprising conclusion: The usage of phase saving and
random selection of polarity during chronological backtracking leads to
indistinguishable runtime performance in terms of instances solved and PAR-2
score.
  We introduce Decaying Polarity Score (DPS) to capture the trend of the
polarities attained by the variable, and upon observing lack of performance
improvement due to DPS, we turn to a more sophisticated heuristic seeking to
capture the activity of literals and the trend of polarities: Literal State
Independent Decaying Sum (LSIDS). We find the 2019 winning SAT solver,
Maple_LCM_Dist_ChronoBTv3, augmented with LSIDS solves 6 more instances while
achieving a reduction of over 125 seconds in PAR-2 score, a significant
improvement in the context of the SAT competition.
