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