pub fn mod_counting(n: usize, q: usize) -> (DimacsCnf, ExpectedVerdict)Expand description
The modular counting principle Count_q(n): can the n-element set {0,…,n−1} be exactly
partitioned into blocks of size q? A Boolean per q-subset (hyperedge); clauses force every
element to lie in ≥ 1 chosen block and forbid any two overlapping blocks — so the chosen blocks
are a perfect q-cover (an exact partition). That exists iff q ∣ n, hence the formula is
UNSAT exactly when q ∤ n. This is the canonical modular family — the obstruction is a
counting argument mod q that resolution cannot make at low width (Ajtai; Beame–Pitassi), the
natural target of the GF(q) / mod-m rung. q = 2 is perfect matching on the complete graph K_n
(UNSAT for odd n). The hyperedge count is C(n, q), so keep n, q small.