Function lll_certifies_sat 

pub fn lll_certifies_sat(clauses: &[Vec<Lit>]) -> Option<LllSatCert>

Certify satisfiability from sparsity via the symmetric LLL. Returns the witnessing degrees when e · 2^{−w_min} · (d+1) ≤ 1; otherwise None (the condition is sufficient, not necessary — None means “this certificate does not apply”, never “UNSAT”). An empty clause set is vacuously SAT; a set containing an empty clause can never be certified (it is UNSAT).