Function solve 

pub fn solve(clauses: &[(Lit, Lit)], num_vars: usize) -> TwoSatOutcome

Decide a 2-SAT instance (clauses of two literals each — a unit clause is (a, a)). Returns a satisfying assignment, or the variable whose SCC contains both polarities.