sat.tex

\def\T{\hbox to 1.5em{\hfill}}
\def\N{\\}
\def\CC#1{&{{\color{black}{// #1}}}}
\def\C#1{\CC{#1} \\}
\def\K#1{\textsf{#1}}
\def\I#1{\mbox{\textrm{#1}}}
\def\L#1{\raise .2ex\hbox{\scriptsize{$#1$}}&}
\begin{tabular}{r@{\qquad}l@{\qquad\quad}l}
%
\L{ 1} \K{function} \I{sat} ($r$, $\sigma$)          \C{returns Boolean value $\BOOLE = \{0,1\}$}
\L{ 2} \T \K{while} $\sigma (r) \neq 1$              \C{while not satisfied}
\L{ 3} \T \T $g = r$, $t = 1$                        \C{initialize path as root path}
\L{ 4} \T \T \K{while} $\neg \I{leaf}(g)$            \C{while current node is an operator}
\L{ 5} \T \T \T $n = \I{child} (\sigma, t, g)$       \C{select backtracing node}
\L{ 6} \T \T \T $x = \I{value} (\sigma, t, g, n)$    \C{select backtracing value}
\L{ 7} \T \T \T $g = n$, $t = x$                     \C{backtracing step (propagation)}
\L{ 8} \T \T \K{if} $\neg \I{constant} (g)$          \C{check if leaf is variable $v = g$}
\L{ 9} \T \T \T $\sigma = \I{update} (\sigma, g, t)$ \C{apply move to variable $v = g$}
\L{10} \T \K{return} $1$                             \CC{return with $1$ (\emph{true}) if satisfied}
%
\end{tabular}