Function decide_2sat 

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

Decide a width-≤2 CNF in polynomial time via the 2-SAT SCC solver. true = satisfiable. An empty clause forces UNSAT. Panics if handed a clause wider than 2 (not a 2-SAT instance).