Skip to main content

solve_polynomial_system_gf2

Function solve_polynomial_system_gf2 

Source
pub fn solve_polynomial_system_gf2(
    eqs: &[Vec<u64>],
    n_vars: usize,
    max_degree: usize,
) -> PolySolveResult
Expand description

Solve a Boolean polynomial system over GF(2) by XL (eXtended Linearization). Each equation is an XOR of monomials (bitmasks over the n_vars variables, x²=x; mask 0 is the constant) that must be 0. For each operating degree d = 1..=max_degree, every equation is multiplied by all monomials of degree ≤ d − deg(eq), the enlarged system is linearized over the degree-≤ d monomials (with the constant pinned to 1) and solved: an inconsistency proves the system unsatisfiable (Refuted), a solution whose degree-1 part satisfies the original equations is returned (Solved), otherwise the degree is raised. This solves systems the plain degree-d linearization cannot, and refutes ones it cannot see contradictory.