Function decide_sat_via_2sat_backdoor 

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

Decide satisfiability through a 2-SAT backdoor: the instance is satisfiable iff some fixing of U leaves a satisfiable 2-SAT residual. This solves in 2^{|U|} polynomial branches instead of a 2ⁿ search — the structure (the backdoor) turned an exponential into a small, easy fan-out. U must be a strong backdoor to 2-SAT (every residual width ≤ 2).