Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Lower Bounds on Inverse Cellular Automata via Proof Complexity

Maryia Kapytka

Abstract

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.

Lower Bounds on Inverse Cellular Automata via Proof Complexity

Abstract

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 . 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.

Paper Structure

This paper contains 29 sections, 26 theorems, 142 equations, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Cellular automata
  4. Propositional proof complexity
  5. Proof systems
  6. Bounded arithmetic
  7. $I\Delta_0$ and $I\Delta_0(R)$
  8. $V^0$
  9. Coding of finite relations and functions
  10. Propositional translation of bounded arithmetic
  11. Paris-Wilkie translation
  12. Coding of CNFs
  13. Reflection principle
  14. Computation table for a formula
  15. Types of cells
  16. ...and 14 more sections

Key Result

Lemma 2.2

(DURAND1994387) For fixed $N$ (of size $v$) the size of a binary string sufficient to code a cellular automaton of dimension $d=2$ is bounded above by $s^v\log s$, where $s$ is the size of $S$. $\blacktriangleleft$$\blacktriangleleft$

Theorems & Definitions (65)

  • Definition 2.1: Cellular automaton
  • Lemma 2.2
  • proof
  • Definition 2.3: Propositional proof system cook1979relative
  • Definition 2.4: p-simulation
  • Definition 2.5: Depth of a formula
  • Example 2.6: Pigeonhole principle
  • Theorem 2.7: Ajtai’s theorem
  • Definition 2.8: $I\Delta_0$
  • Definition 2.9: $2$-BASIC
  • ...and 55 more