Certified XOR-Spectral Normalization for SAT: Entailed Parity Detection, Elimination, and DRAT-Compatible Progress
Fuente:
Zenodo
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Recurso digital |
| Publié: |
Zenodo
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866901998207500288 |
|---|---|
| author | Paradise, Christopher |
| author_facet | Paradise, Christopher |
| contents | <p class="p1">This paper presents a sound algebraic theory module for SAT based on entailed XOR normalization. It defines verifier-checkable XOR-witness certificates, an XOR store represented as a linear system over <span class="s1">\mathbb{F}_2</span>, Gaussian elimination for inconsistency and consequence derivation, and an XOR-LEARN step that can compile newly derived parity consequences back into CNF with checker-accepted implication proofs. The module is intentionally bounded: it does not assume that all hard SAT structure is linear, but when entailed parity is present it provides a certified progress move compatible with DRAT/FRAT-style proof checking. Its contribution is methodological: a concrete algebraic auxiliary layer sitting between clause-based proof systems and linear structure, with explicit soundness guarantees and clean integration into a verifier-driven SAT router.</p> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_19508205 |
| institution | Zenodo |
| language | |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | Certified XOR-Spectral Normalization for SAT: Entailed Parity Detection, Elimination, and DRAT-Compatible Progress Paradise, Christopher certified XOR normalization, SAT proof systems, entailed parity detection, XOR elimination, DRAT-compatible learning, FRAT-compatible implications, algebraic SAT methods, Gaussian elimination over F2, certificate-driven SAT, auxiliary theory modules <p class="p1">This paper presents a sound algebraic theory module for SAT based on entailed XOR normalization. It defines verifier-checkable XOR-witness certificates, an XOR store represented as a linear system over <span class="s1">\mathbb{F}_2</span>, Gaussian elimination for inconsistency and consequence derivation, and an XOR-LEARN step that can compile newly derived parity consequences back into CNF with checker-accepted implication proofs. The module is intentionally bounded: it does not assume that all hard SAT structure is linear, but when entailed parity is present it provides a certified progress move compatible with DRAT/FRAT-style proof checking. Its contribution is methodological: a concrete algebraic auxiliary layer sitting between clause-based proof systems and linear structure, with explicit soundness guarantees and clean integration into a verifier-driven SAT router.</p> |
| title | Certified XOR-Spectral Normalization for SAT: Entailed Parity Detection, Elimination, and DRAT-Compatible Progress |
| topic | certified XOR normalization, SAT proof systems, entailed parity detection, XOR elimination, DRAT-compatible learning, FRAT-compatible implications, algebraic SAT methods, Gaussian elimination over F2, certificate-driven SAT, auxiliary theory modules |
| url | https://doi.org/10.5281/zenodo.19508205 |