pub fn build_ns_certificate_zm(
m: u64,
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Result<NsCertificateZm, Vec<bool>>Expand description
The uniform completeness construction over ℤ/m — partition-of-unity charging, valid over any
commutative ring because it never divides. Returns a constructive certificate proving UNSAT or a
satisfying assignment proving SAT: a total, certifying decision over every modulus m ≥ 2 — so
“structureless” (no certificate at any degree ≤ n) has no witness among finite formulas over
any ℤ/m. The honest cost is unchanged: the certificate lives in the 2ⁿ monomial basis
(existence, not efficiency), and num_vars ≤ 20 bounds the explicit-corner construction.