Function covering_collapse 

pub fn covering_collapse(
    num_vars: usize,
    formula: &[Vec<Lit>],
    items: usize,
    bins: usize,
) -> RankedRefutation

Drive the steered Heule descent over a discovered items × bins covering layout: bins + 1 items are a tight pigeonhole, so force them out of the bins one at a time, each ¬var(i, bin) certified by “swap item i with the last active item.” Returns the ranked refutation; every step is PR-self-checked, so a layout that is not really a covering problem simply fails to refute.