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.

翻译：我们研究有界构型上逆元胞自动机的复杂度问题。根据Durand定理，在此设定下判定单射性是co-NP完全的。我们通过从UNSAT到该问题的直接归约（避免更复杂的中间构造），给出了该定理的一个更简洁的证明。我们同时证明，归约的一个方向可以在有界算术的弱理论$V^0$中形式化。Durand的co-NP完全性结果允许将作用于有界构型上的逆元胞自动机视为命题证明（参见Cavagnetto），并证明其大小下界。该证明利用了有界深度Frege系统的已知下界，以及Paris-Wilkie将算术证明转化为命题证明的翻译方法，从而将证明复杂度下界迁移至我们的设定中。