pub fn emit_drat_over_support(
clauses: &[Vec<Lit>],
support: &BTreeSet<u32>,
) -> Option<Vec<Vec<Lit>>>Expand description
Resolution-refute the sub-CNF confined to the support variables — the convention-agnostic bridge.
The emitted clauses are resolvents of real CNF clauses, so each is RUP against the original
formula by construction and a drat-trim check holds. None if that sub-CNF is not UNSAT (so the
caller’s algebraic verdict could not be reproduced clausally — a fail-closed signal).