Struct NsCertificate 

pub struct NsCertificate { /* private fields */ }

A constructive Nullstellensatz certificate over the multilinear GF(2) ring: one coefficient polynomial g_C per input clause such that Σ_C p_C · g_C = 1, where p_C = clause_polynomial(C) is the clause’s false-indicator. The identity is a re-checkable proof of UNSAT — evaluate it at any assignment a: the right side is 1, so some p_C(a) = 1, i.e. every assignment falsifies some clause. Where nullstellensatz_refutes only decides whether such a certificate exists, this one carries the witness.

Implementations

impl NsCertificate

pub fn num_vars(&self) -> usize

The variable count the certificate lives over.

pub fn degree(&self) -> usize

The maximum monomial degree among the coefficient polynomials. Multilinear over num_vars variables, so ≤ num_vars unconditionally — the content is not this (trivial for a multilinear certificate) but that the certificate exists and is built by one uniform construction at every n.

pub fn verify(&self, clauses: &[Vec<Lit>]) -> bool

Re-check against the original clauses (zero trust in the producer): recompute Σ_C clause_polynomial(C) · g_C and confirm it is the constant 1 (the empty monomial). A true verdict is an independent proof that clauses is unsatisfiable; it fails closed if the certificate’s clause count does not match the formula it is checked against.

Trait Implementations

impl Clone for NsCertificate

fn clone(&self) -> NsCertificate

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for NsCertificate

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.