Module ordering 

The ordering-principle specialist — a polynomial-time recognizer + refuter for GT(n), the linear-ordering contradiction. GT(n) asserts a strict total order (totality + antisymmetry + transitivity) in which every element has a strictly greater one (“no maximum”). That is impossible: a finite strict total order always has a maximum. So a complete GT(n) core is unsatisfiable, and any formula containing it (a superset of an UNSAT core) is UNSAT.

The general cascade decides GT(n) only by super-polynomial search (measured: GT(20) ≈ 2.7s, ~68k conflicts, growing ~10x every 4 steps). This module recognizes the structure directly and certifies UNSAT from it — polynomial, and instant where search walls.

Soundness is by faithful, conservative recognition, in the style of crate::pigeonhole: the recognizer verifies, for a single consistent element/edge identification, that ALL of totality, antisymmetry, transitivity (every ordered triple), and the no-maximum clause (every element) are present. Only then is a complete GT(n) core certified present — and it is genuinely UNSAT. Any missing, ambiguous, or extra-shaped piece makes the recognizer return None (never a false refutation); the caller then falls through to the general engine. Full transitivity is essential: without it a “no-maximum tournament” can be a satisfiable cycle (e.g. 0<1<2<0), so an incomplete structure must not be refuted.

The refutation object is an OrderingCert: the element/edge identification, which a checker re-verifies against the raw clauses (check_ordering_cert) with zero trust in how it was produced.

Structs

OrderingCert

A re-checkable ordering-principle refutation: the recovered element/edge identification of a complete GT(n) core. edge[i * n + j] is the comparison variable x_ij (“i < j”) for the ordered pair (i, j); diagonal entries (i == j) are u32::MAX and unused. Given this map a checker re-verifies that every totality, antisymmetry, transitivity, and no-maximum clause is present — the whole certificate, no trust in the recognizer.

Functions

check_ordering_cert

Re-check an OrderingCert against the raw clauses from scratch, trusting nothing about how it was produced: verify that for its element/edge identification EVERY totality, antisymmetry, transitivity, and no-maximum clause is present. true iff the certificate genuinely witnesses a complete GT(n) core (which is unsatisfiable), so the formula is UNSAT.

ordering_certificate

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.

refute_ordering

Refute a formula that contains a complete ordering-principle core. true iff a certificate is recovered — see ordering_certificate. Never a false refutation.

refutes_ordering_principle

The ordering cut over a ProofExpr: clausify and run the specialist. This is the entry the cascade (crate::sat::prove_unsat) calls.