Skip to main content

clause_polynomial_gfp

Function clause_polynomial_gfp 

Source
pub fn clause_polynomial_gfp(f: NsField, clause: &[Lit]) -> GfpPoly
Expand description

The clause polynomial over f — the signed false-indicator: a positive literal x contributes 1 − x (over GF(3): 1 + 2x, not 1 + x — over GF(2) the two coincide, which is exactly the sign the general engine must make explicit), a negative literal ¬x contributes x. The product is 1 exactly on the clause’s falsifying corners and 0 elsewhere, over every field.