Lower Bounds on Inverse Cellular Automata via Proof Complexity
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912995818340352 |
|---|---|
| author | Kapytka, Maryia |
| author_facet | Kapytka, Maryia |
| contents | We study the complexity of inverse cellular automata on configurations of bounded size. Deciding injectivity in this setting is co-NP-complete by a theorem of Durand. We give a simpler proof of this theorem by a direct reduction from UNSAT to this problem, avoiding more complicated intermediate constructions. We also show that one direction of the reduction can be formalized in the weak theory of bounded arithmetic $V^0$. Durand's coNP-completeness result allows one to view inverse cellular automata acting on bounded size configurations as propositional proofs, cf. Cavagnetto, and we prove lower bounds on their size. The proof uses known lower bounds for bounded-depth Frege systems together with the Paris--Wilkie translation of arithmetic proofs into propositional proofs, which allows us to transfer proof complexity lower bounds to our setting. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_01041 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Lower Bounds on Inverse Cellular Automata via Proof Complexity Kapytka, Maryia Logic Discrete Mathematics Logic in Computer Science F.2.0 We study the complexity of inverse cellular automata on configurations of bounded size. Deciding injectivity in this setting is co-NP-complete by a theorem of Durand. We give a simpler proof of this theorem by a direct reduction from UNSAT to this problem, avoiding more complicated intermediate constructions. We also show that one direction of the reduction can be formalized in the weak theory of bounded arithmetic $V^0$. Durand's coNP-completeness result allows one to view inverse cellular automata acting on bounded size configurations as propositional proofs, cf. Cavagnetto, and we prove lower bounds on their size. The proof uses known lower bounds for bounded-depth Frege systems together with the Paris--Wilkie translation of arithmetic proofs into propositional proofs, which allows us to transfer proof complexity lower bounds to our setting. |
| title | Lower Bounds on Inverse Cellular Automata via Proof Complexity |
| topic | Logic Discrete Mathematics Logic in Computer Science F.2.0 |
| url | https://arxiv.org/abs/2604.01041 |