Function pure_literal_reduce 

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

Cut out the autark sections. A pure literal (a variable appearing in only one polarity) is the simplest autarky: assigning it satisfies every clause it touches, so that whole section of the cube is removed without affecting satisfiability. Iterate to a fixpoint and what remains is the hard core — the part with no free section to cut. Returns (core clauses, assigned pure literals). Sound: pure- literal elimination preserves satisfiability (Davis–Putnam).