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