Saved in:
| Main Author: | |
|---|---|
| Format: | Recurso digital |
| Language: | English |
| Published: |
Zenodo
2025
|
| Subjects: | |
| Online Access: | https://doi.org/10.5281/zenodo.17008332 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866902139280818176 |
|---|---|
| author | Oertel, Jacob S. |
| author_facet | Oertel, Jacob S. |
| contents | <p>We construct a time-bounded, self-referential SAT instance $\phi$ by synthesizing the Cook-Levin theorem with Kleene's recursion theorem. The resulting formula is satisfiable if and only if a given Turing machine $D$ rejects the description of $\phi$ within a time budget $T$. We provide explicit polynomial bounds on the size of $\phi$ in terms of the descriptions of $D$ and $T$.</p> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_17008332 |
| institution | Zenodo |
| language | eng |
| publishDate | 2025 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | Time-Bounded SAT Fixed Point with Explicit Cook-Levin Accounting Oertel, Jacob S. Computers Computer Systems <p>We construct a time-bounded, self-referential SAT instance $\phi$ by synthesizing the Cook-Levin theorem with Kleene's recursion theorem. The resulting formula is satisfiable if and only if a given Turing machine $D$ rejects the description of $\phi$ within a time budget $T$. We provide explicit polynomial bounds on the size of $\phi$ in terms of the descriptions of $D$ and $T$.</p> |
| title | Time-Bounded SAT Fixed Point with Explicit Cook-Levin Accounting |
| topic | Computers Computer Systems |
| url | https://doi.org/10.5281/zenodo.17008332 |