diff --git a/src/year1/combinatorial-decision-making-and-optimization/module1/sections/_sat.tex b/src/year1/combinatorial-decision-making-and-optimization/module1/sections/_sat.tex index 08a16f0..e01e751 100644 --- a/src/year1/combinatorial-decision-making-and-optimization/module1/sections/_sat.tex +++ b/src/year1/combinatorial-decision-making-and-optimization/module1/sections/_sat.tex @@ -281,6 +281,7 @@ DPLL with two improvements: \begin{remark} Any cut that separates sources (decision literals) and the sink (contradiction node) is a valid conflict clause for backjumping. + \indenttbox \begin{example} \phantom{} \begin{center} \includegraphics[width=0.55\linewidth]{./img/_cdcl_cut.pdf}