Function decompose_and_crush 

pub fn decompose_and_crush(num_vars: usize, clauses: &[Vec<Lit>]) -> bool

Decompose into independent components and crush: return true (UNSAT) the moment any component is refuted by a certified cut, never having examined the rest. Isolating a structured UNSAT component unlocks a cut the monolithic formula hides.