Module families 

Parametric generators for symmetry-rich SAT families — the canonical hard cases where symmetry breaking earns its keep. They are programmatic (reproducible, offline, parametric) rather than vendored .cnf files, and each is pinned to its known verdict so the solver and the certified pipeline can be tested against ground truth.

Enums

ExpectedVerdict

The known verdict of a generated instance, for test oracles.

Functions

clique_coloring

Graph k-coloring of the complete graph K_n — the canonical color-permutation symmetry family (the color group S_k acts, on top of the vertex group S_n). It is unsatisfiable exactly when k < n (a clique of size n needs n colors). The variable “vertex v takes color c” lives at index v*k + c.

functional_php

The functional pigeonhole principle FPHP(n): php(n) strengthened so each pigeon sits in at most one hole (the placement is a function, not a relation). Adds the “no pigeon in two holes” clauses on top of PHP; still UNSAT, still S_n × S_{n−1}-symmetric, and the standard strengthening used to check that symmetry breaking survives the extra functional clauses. Same layout as php.

grid_tseitin

The Tseitin formula on a w × n grid with odd total charge — UNSATISFIABLE, and the sharpest indictment of resolution search there is. A grid has treewidth exactly w (a fixed constant, independent of the length n), so a POLYNOMIAL-size, bounded-width resolution refutation provably EXISTS. Yet CDCL solvers without Gaussian reasoning blow up on the parity regardless — they cannot find the short proof that is known to exist — while Gaussian elimination over GF(2) decides it in near-linear time. One Boolean per grid edge; per vertex, the XOR of its incident edges equals its charge (vertex 0 charged, the rest not — an odd sum, hence inconsistent). Returns the XOR system (for crate::xorsat) and the equisatisfiable CNF.

ksat_threshold_first_moment_upper

The first-moment (counting) upper bound on the random k-SAT satisfiability threshold: α*(k) = ln 2 / ln(2ᵏ / (2ᵏ − 1)). Above this clause density the expected number of satisfying assignments E[X] = 2ⁿ(1 − 2⁻ᵏ)^{αn} = (2·(1 − 2⁻ᵏ)^α)ⁿ has per-variable base < 1, so E[X] → 0 and the instance is UNSAT with high probability (Markov) — a rigorous upper bound on the true threshold, exact and closed-form (no sampling). The sequence climbs as 2ᵏ ln 2 − (ln 2)/2, asymptotically doubling per k: 2.41, 5.19, 10.74, 21.83, 44.02, … for k = 2, 3, 4, 5, 6, …. The true thresholds (≈ 1, 4.27, 9.93, 21.1, …) lie below it; the gap → ½ as k → ∞ (the difference between the first-moment bound 2ᵏln2 − ½ln2 and the sharp value 2ᵏln2 − (1+ln2)/2).

mod_counting

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.

mod_counting_edges

The edge layout of mod_counting: variable e is the q-subset mod_counting_edges(n, q)[e] of the point set {0,…,n−1} — the map a witness-support predicate needs to read a monomial as a set of blocks.

mod_counting_groups

The exactly-one groups of mod_counting’s linear encoding: for each point, the variables of its covering clause — the incident q-subsets, in the same variable order as mod_counting. Feed to polycalc::exactly_one_linear_generators for the degree-1 point generators plus overlap pairs (the encoding the modular-counting degree lower bounds are stated against).

mod_m_tseitin_expander

The composite-modulus sibling of mod_p_tseitin_expander: the same total-charge-2 divergence obstruction over ℤ/m for a squarefree composite m (e.g. m = 6), with a mixed-radix one-hot Boolean encoding (m values per edge). By CRT ℤ/m ≅ ∏ GF(pᵢ), so the system is inconsistent over ℤ/m exactly when it is inconsistent over some prime factor — total charge 2 ≢ 0 (mod m) for any m ≥ 3 that does not divide 2 — and crate::modm::solve decides it through that factor with a solver-free re-checkable certificate (crate::modm::is_refutation). This drives the ring route (ℤ/m Gaussian via CRT), not the prime-field route, on a CNF that resolution still walls on.

mod_p_consistent_onehot

A satisfiable sibling of mod_p_tseitin_expander over the same 3-regular graph and the same one-hot Boolean encoding, but with a charge distribution whose total ≡ 0 (mod p). The divergence system Σ_out x − Σ_in x ≡ charge(v) is consistent exactly when the charges sum to zero (summing all vertex equations telescopes the left side to 0), so this instance is SAT — the control for the GF(p) route’s model-returning path. Charge: +1 at vertex 0, −1 (= p−1) at vertex 1, zero elsewhere.

mod_p_tseitin_expander

The mod-p Tseitin obstruction on a random 3-regular expander — the parity crush carried to every prime. Each edge carries a GF(p) flow variable; orient each edge and impose, at every vertex, the signed divergence Σ_out − Σ_in ≡ charge (mod p). Summing all vertices telescopes the edge variables to 0, so the system is inconsistent exactly when the total charge ≢ 0 (mod p). We charge two vertices (total 2): inconsistent over GF(p) for every odd prime p, yet consistent over GF(2) (2 ≡ 0) — a family the parity cut is structurally blind to, decided instantly by Gaussian elimination over the right GF(p), and (on an expander) exponentially hard for resolution. Returns the GF(p) system (for crate::modp), the equisatisfiable one-hot Boolean CNF (for resolution solvers), and the GF(p) verdict.

mutilated_chessboard

The mutilated chessboard: an n×n board with two OPPOSITE corners removed, asking for a perfect domino tiling. Every domino covers one black and one white square, but the two removed corners share a colour (for even n), so the black/white counts differ by two and no tiling exists — UNSAT, and a textbook resolution-exponential family. The infeasibility is a bipartite-matching (Hall) obstruction, which our covering route certifies in polynomial time. Variables are dominoes (grid edges between adjacent surviving squares); each surviving square must be covered by exactly one. n must be even (so the parity argument bites).

onto_php

The onto (bijective) pigeonhole principle onto-FPHP(n): functional_php(n) further forced to be onto — every hole receives at least one pigeon. The placement is now a bijection n → n−1, which cannot exist; UNSAT. This is the hardest standard PHP variant for symmetry reasoning (it pins both the pigeon and the hole side), and the maximal clause set over the shared php layout.

ordering_principle

The linear ordering principle GT(n): no finite strict total order lacks a maximal element — yet this formula asserts exactly that, so it is UNSAT. x[i][j] (index i*n + j) reads “i < j”. Antisymmetry + totality + transitivity force a linear order, and the “every element has a greater one” clauses then contradict finiteness. A canonical resolution-hard family — it stresses the CDCL core / cutting-plane reasoning rather than a matching or parity specialist.

parity_exactly_one

Coupled exactly-one + parity — a scalable MIXED family that needs BOTH structures at once. The selectors x₀…x_{n-1} are constrained to exactly one true (an at-most-one clique + an at-least-one clause — a cardinality covering) AND to even total parity ⊕ xᵢ = 0 (a GF(2) system, encoded by a width-3 prefix-XOR chain with auxiliaries sᵢ = ⊕_{j≤i} xⱼ plus the unit s_{n-1} = 0). Exactly-one forces an ODD selector count, the parity forces EVEN — UNSAT, yet neither substructure alone is (the parity chain is satisfiable, exactly-one is satisfiable). The canonical shape for the fused parity+cardinality route (crate::lyapunov::fused_parity_cardinality_decide); 2n variables.

parity_unsat

A guaranteed-unsatisfiable random 3-XOR (parity) system — the k = 3 case of random_kxor: at least m 3-XOR equations over n variables, all consistent with a planted assignment except one flipped row, built up to maximal GF(2) rank so the inconsistency holds for any seed (see random_kxor for why the naive single flip does not suffice). Full-rank 3-XOR above the XOR-SAT threshold is exponentially hard for resolution (Ben-Sasson–Wigderson 2001), hence for every CDCL solver — yet linear for Gaussian elimination over GF(2). Returns the XOR equations (for crate::xorsat) and the equisatisfiable CNF (for a resolution solver).

pebbling_pyramid

The pebbling contradiction on the pyramid DAG of the given height — the canonical resolution space family (Ben-Sasson–Wigderson; Nordström). The pyramid has rows 0..=height with row r holding r+1 nodes; each node (r, i) for r < height has the two predecessors (r+1, i) and (r+1, i+1) below it. One Boolean per node “is pebbled”: every source (bottom row) is asserted pebbled (unit), pebbling propagates up (pebbled(a) ∧ pebbled(b) → pebbled(parent)), and the apex (0,0) is asserted unpebbled — a contradiction, so UNSAT. Refutation size is linear (unit propagation alone closes it), but refuting it in small space provably is not — the axis pigeonhole and parity do not touch.

php

The pigeonhole principle PHP(n): n pigeons into n-1 holes — unsatisfiable, and the textbook symmetry / resolution-hard family (any resolution refutation is exponential, while breaking the S_n × S_{n-1} symmetry collapses it). The variable for “pigeon p sits in hole h” lives at index p*(n-1) + h, so pigeons index rows and holes index columns.

ramsey

The Ramsey formula Ramsey(s, t; n): 2-colour the edges of the complete graph K_n (one Boolean per edge — true = red, false = blue) avoiding every red K_s and every blue K_t. For each s-clique a clause forbids all its edges being red; for each t-clique a clause forbids all blue. Such a colouring exists iff n < R(s, t), so the formula is UNSAT exactly when n ≥ R(s, t). A genuinely different geometry from pigeonhole/parity — clique structure, not covering or counting — and a classic CDCL stress family (Ramsey(3,3;6) is the smallest UNSAT case). Panics for (s, t) whose Ramsey number is unknown (so the verdict is never guessed); see ramsey_number.

ramsey_number

The known two-colour Ramsey numbers R(s, t) for the small (s, t) we can actually build CNFs for (symmetric: R(s, t) = R(t, s)); None when the value is still an open problem. R(s, t) is the least n such that every red/blue colouring of K_n’s edges contains a red K_s or a blue K_t.

random_3sat

A random 3-SAT instance: num_clauses clauses of three distinct variables with random signs, over vars variables, from a seeded SplitMix64 stream (reproducible — no wall-clock). Near the clause/variable ratio 4.26 these are the canonical hard, non-symmetric benchmarks — the general-instance control where raw CDCL quality (not symmetry breaking) decides the race.

random_ksat

A random k-SAT instance: num_clauses clauses of k distinct variables with random signs, over vars variables, from a seeded SplitMix64 stream (reproducible — no wall-clock). Generalizes random_3sat. The satisfiability threshold climbs with k roughly as α_k ≈ 2ᵏ ln 2 (≈ 4.27 for k=3, ≈ 9.93 for k=4, ≈ 21.1 for k=5). Requires k ≤ vars.

random_kxor

A guaranteed-unsatisfiable random k-XOR (parity) system over n variables: at least m equations of k distinct variables, all consistent with a planted assignment p except one whose right-hand side is flipped. Generalizes parity_unsat (the k = 3 case).

tseitin_expander

The Tseitin formula on a random 3-regular expander with odd total charge — UNSATISFIABLE, exponentially hard for resolution (so every CDCL solver blows up), yet solved in polynomial time by Gaussian elimination over GF(2). A non-pigeonhole hard family: the hardness is parity / graph expansion, not covering symmetry. One Boolean per edge; per vertex, the XOR of its incident edges equals that vertex’s charge (vertex 0 charged, the rest not — an odd sum, hence inconsistent). Returns the XOR system (for crate::xorsat) and the equisatisfiable CNF.

weak_php

The weak pigeonhole principle PHP^{holes}_{pigeons}: pigeons pigeons into holes holes — unsatisfiable exactly when pigeons > holes. Generalizes php (which is the tight holes = pigeons − 1 case) to any hole count, including the weak regime (holes = 2·pigeons, pigeons², …) used to probe how far symmetry breaking scales as the holes-to-pigeons ratio grows. Same variable layout as php — “pigeon p in hole h” at index p*holes + h — so weak_php(n, n−1) is byte-for-byte php(n).