pub fn cardinality_collapse( num_vars: usize, formula: &[Vec<Lit>], ) -> Option<(Vec<u64>, bool, usize)>