@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@inproceedings{SM20,
  title={Designing New Phase Selection Heuristics},
  author={Shaw, Arijit and Meel, Kuldeep S.},
  booktitle=SAT,
  month=jul,
  bib2html_rescat={Solver Engineering},
  bib2html_pubtype={Refereed Conference},
  bib2html_dl_pdf={../Papers/sat20-sm.pdf},
  code={https://github.com/meelgroup/duriansat},
  year={2020},
  abstract={
    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.
  },
}