Skip to main content

check_sos_certificate

Function check_sos_certificate 

Source
pub fn check_sos_certificate(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    cert: &BTreeMap<usize, i128>,
) -> bool
Expand description

Independently re-check an SoS Farkas certificate from sos_certificate: recompute the degree-2 lift from the clauses, combine its polynomials with the certificate’s multipliers, and confirm the result cancels every variable and leaves a strictly positive constant — the self-contained contradiction 0 < d ≤ 0. It shares no arithmetic with the Fourier–Motzkin elimination that produced the certificate, so it is a genuine independent witness of the refutation (the SoS analog of crate::xorsat::is_refutation). Fails closed on a negative multiplier, an out-of-range row, an empty certificate, or any residual variable.