Broken Inline LaTeX

[klmentzer]

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)$).

In Branching/Searching:

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.

[d-krupke]

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 :)