\NeedsTeXFormat{LaTeX2e}
\documentclass{article}
\usepackage[boxed,ruled,vlined]{algorithm2e}
\usepackage{xcolor}
\begin{document}
\begin{algorithm}
\KwOut{satisfiability of the given CNF}
\SetKwComment{Comment}{}{}
\BlankLine
\Begin{
\While{there is an unassigned or unpropagated var}{
  \If{there is no unpropagated var}{
    select a decision var and its phase\;
  }
  \uIf{BCP() returns an conflict}{
    \If{decision level is root level}{
      \Return{UNSAT}\;
    }
    CONFLICT-ANALYSIS()\;
    BACKTRACK()\;
  }
  \If{restart condition holds or the current stage ends}{
    RESTART()\;
    \If{a new stage begins}{
        REDUCE()\;
        update restart conditions\;
        \If{a new cycle begins}{
            VIVIFY()\;
            select var phases\;
            \If{a new segment begins}{
                ELIMINATE()\;
                rescale var activities\;
            }
        }
    }
  }
}
\Return{SAT}\;
}
\caption{Main search loop in Splr-0.17 (src/solver/search.rs)}
\end{algorithm}
\end{document}