optional · interactive figures

21

Explore: lazy clause generation

The order encoding and a precedence explaining its bounds, and a CDCL run that learns a clause mixing a Boolean with a bound.

optional: nothing in the lab depends on itback to the slides

21 · explore

The order encoding, and one precedence

Try: decide x ≥ 2 and read the explanation clause; then pull y ≤ 4 and get a conflict. Static versions: the order encoding, explanations.

21 · explore

A learned clause mixing a Boolean and a bound

Try: step to the explanation that is already false, then the analysis, which learns (¬b ∨ [a≤1]). Static version: Explanations, on one precedence.