pub fn find_pr_clause(
num_vars: usize,
clauses: &[Vec<Lit>],
alpha: &[Lit],
) -> Option<(Vec<Lit>, Witness)>Expand description
From a “stuck” partial assignment alpha (its true-literals), try to discover a PR clause
C = ¬alpha that blocks it, via the positive reduct. Returns the clause and its witness, both
verified by the PR checker (fail-closed). This is the SDCL primitive — a universal,
automorphism-free generalization of certified symmetry breaking.