pub fn ordering_certificate(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Option<OrderingCert>Expand description
Recover a complete ordering-principle (GT(n)) core from clauses, or None if there is none. On
Some(cert) the formula is unsatisfiable (a finite strict total order has a maximum, contradicting
the no-maximum clauses), and cert re-checks via check_ordering_cert. Conservative / fail-closed
— never a false certificate. See the module docs.