Skip to main content

build_ns_certificate_gfp

Function build_ns_certificate_gfp 

Source
pub fn build_ns_certificate_gfp(
    f: NsField,
    num_vars: usize,
    clauses: &[Vec<Lit>],
) -> Result<NsCertificateGfp, Vec<bool>>
Expand description

The uniform completeness construction over f — the partition-of-unity charging of crate::polycalc::build_ns_certificate, field-generic because its every ingredient is: the signed point indicators sum to 1 in any field (partition_of_unity_gfp), and p_C · δ_a = δ_a whenever p_C(a) = 1 (multilinear representations on the cube are unique over any field). Returns a constructive NsCertificateGfp proving UNSAT or a satisfying assignment proving SAT. Bounded to num_vars ≤ 20 (the explicit-corner construction).