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