pub fn onto_php(n: usize) -> (DimacsCnf, ExpectedVerdict)Expand description
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.