SatisfiableXOR
plain-language theorem explainer
SatisfiableXOR defines the property that a CNF formula paired with an XOR system over n variables admits a Boolean assignment satisfying both. Researchers analyzing hybrid SAT problems with parity constraints would cite this definition when formalizing mixed constraint systems. It is expressed directly as an existential quantifier over assignments that pass CNF evaluation and satisfy every XOR parity condition.
Claim. Let $ψ = (φ, H)$ where $φ$ is a CNF formula on $n$ variables and $H$ is an XOR system. Then $ψ$ is satisfiable when there exists an assignment $a$ such that $evalCNF(a, φ)$ evaluates to true and $a$ satisfies every constraint in $H$.
background
CNFWithXOR is a structure that pairs a standard CNF formula $φ$ with an XORSystem $H$ without rewriting the parity constraints into clauses. An Assignment maps each of the $n$ variables to a Boolean value. evalCNF returns true precisely when every clause of $φ$ is satisfied under the assignment. satisfiesSystem holds when the parity of the assigned values on each subset in $H$ matches the prescribed target parity. The module introduces XOR constraints as parity conditions on variable subsets and places this definition in the broader setting of SAT encodings that retain semantic XOR structure.
proof idea
This is a direct definition that encodes the joint satisfiability condition as an existential statement over Assignment n, conjoining the CNF evaluation predicate with the satisfiesSystem predicate on the XOR component.
why it matters
The definition supplies the semantic notion of satisfiability for CNF formulas extended by XOR parity constraints, forming a basic interface in the Complexity.SAT.XOR module. It supports downstream analysis of hybrid constraint problems that may later connect to cost-algebraic or functional-equation machinery imported from CostAlgebra and FunctionalEquation. No immediate parent theorems are recorded, indicating it serves as foundational scaffolding for further complexity results within Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.