pub fn gadget_clauses(eq: &XorEquation) -> Vec<Vec<Lit>>Expand description
The full parity gadget of eq: one clause per wrong-parity assignment of its variables. These are
exactly the CNF clauses a Tseitin/XOR encoding carries for the constraint.
pub fn gadget_clauses(eq: &XorEquation) -> Vec<Vec<Lit>>The full parity gadget of eq: one clause per wrong-parity assignment of its variables. These are
exactly the CNF clauses a Tseitin/XOR encoding carries for the constraint.