Constraint Pattern - At Most One

Sometimes you need "at most one of x, y, z is true." How do you represent this in $2$-SAT where clauses have two literals?

Break it into pairwise constraints: "NOT x OR NOT y", "NOT x OR NOT z", "NOT y OR NOT z". Each pair says "you cannot pick both of these." Together they enforce at most one. Add all pairwise edges to the graph. For k variables, this creates $k(k-1)/2$ clauses. Works well for small k.