CNFWithXOR
plain-language theorem explainer
CNFWithXOR pairs a CNF formula over n variables with a list of XOR parity constraints on the same variables. Researchers analyzing hybrid SAT problems with linear parity conditions would cite this structure when extending satisfiability to combined clause and GF(2) systems. The definition is a direct record type with no computational content or proof obligations.
Claim. For a natural number $n$, a CNFWithXOR instance consists of a CNF formula $φ$ (a list of clauses) together with an XORSystem $H$ (a list of parity constraints, each requiring the XOR of a variable subset to equal a fixed parity).
background
The module defines XOR constraints over n variables as parity conditions on subsets. XORSystem is the abbreviation List (XORConstraint n). CNF is the imported structure whose clauses field holds a list of clauses over n variables, while Satisfiable asserts existence of an assignment a such that evalCNF a φ evaluates to true. The local setting pairs these objects semantically rather than converting XOR constraints into additional CNF clauses.
proof idea
This is a structure definition with exactly two fields: φ of type CNF n and H of type XORSystem n. No lemmas are applied and no tactics are used; the declaration is a direct record construction.
why it matters
CNFWithXOR supplies the input type for SatisfiableXOR (existence of an assignment satisfying both evalCNF on φ and satisfiesSystem on H) and UniqueSolutionXOR (the same predicate strengthened to uniqueness). It enables semantic combination of standard CNF satisfiability with XOR parity systems, supporting uniqueness analysis in the SAT-XOR module without clause expansion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.