pindakaas is a collection of encoders to transform integer and
pseudo-Boolean (PB) constraints into conjunctive normal form (CNF). It
currently considers mostly linear constraints, which are in the form ∑
aᵢ·xᵢ ≷ k, where the aᵢ's and k are constant, xᵢ's are integer
variables or boolean literals, and ≷ can be the relationship ≤, =, or
≥. Two forms of PB constraints are seen as special forms of PB
constraints: ensuring a set of booleans is At Most One (AMO) or At Most K
(AMK). Specialised encodings are used when these cases are detected.