Function search_cost 

pub fn search_cost(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    use_cut: bool,
    budget: usize,
) -> SearchCost

Run the branch engine purely to measure its size, with use_cut selecting whether the certified cuts fire, and a hard budget on visited nodes so a resolution-class explosion is recorded as Exceeded instead of running forever. With the cut off this is raw DPLL (resolution-strength); with it on, the certified cut closes whole subtrees. The apples-to-apples gap between the two is the campaign’s thesis, quantified.