Wedi'i Gadw mewn:
| Prif Awdur: | |
|---|---|
| Fformat: | Recurso digital |
| Iaith: | |
| Cyhoeddwyd: |
Zenodo
2026
|
| Pynciau: | |
| Mynediad Ar-lein: | https://doi.org/10.5281/zenodo.19508205 |
| Tagiau: |
Ychwanegu Tag
Dim Tagiau, Byddwch y cyntaf i dagio'r cofnod hwn!
|
Tabl Cynhwysion:
- <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>