Broken Inline LaTeX
klmentzer opened this issue · 1 comments
Thank you for putting together this extremely helpful primer! In reading through your work, I just found a few spots with broken inline latex I thought I'd point out.
In DPLL and Unit Propagation :
If we have a clause
$(x_1\vee x_2 \vee \overline{x_3})$ and we have
In LCG Encoding:
Because otherwise we would need a quadratic amount of consistency constraints ($[x=v] \rightarrow [x\not=v'] \forall v\not=v' \in D(x)$).
The arrows pointing towards a node can be seen as conjunctive implication clauses (
$x\wedge y \Rightarrow z$ ), that are added lazily by the propagators.
Thanks again for your help in figuring out what CP-SAT does under the hood.
Glad that you found it helpful! I hope I will find some time to finish it soon. There are unfortunately still some parts that are incomplete or imprecise.
I fixed the broken inline latex (at least it seems to work in my browser now), thanks for telling me :)