Anders Mörtberg: On the algorithmic complexity of contortion solving

Abstract: On March 1 2023 Maximilian Doré visited me and gave a CompMath seminar [1]. In the seminar Max(imilian) discussed some combinatorial problems that occur all the time when working in Cubical Agda. These "contortion problems" are essentially asking how to find a logical formula which allows the system to turn a low dimensional cube (e.g. a line, square, 3D cube, ...) into a higher dimensional cube with an already specified boundary. The goal of Max's visit was to find new algorithms for solving this type of problems and implement them as solvers in Cubical Agda. However, the visit took an unexpected turn after the seminar where Marc asked some very interesting questions about the computational complexity of the problems that we hadn't thought about before. This motivated me, Max and Evan Cavallo to brush up on our algorithmic complexity theory and we eventually managed to prove that contortion solving is NP-complete using a reduction from 3-SAT (Prop 11 in [2]). We have since generalized this to all known cubical type theories and analyzed the computational complexity of the corresponding contortion problems (and much more) in [3]. In the talk I will explain the combinatorics of contortion solving and explain the proof of NP-completeness. I will not assume any prior knowledge of Cubical Agda or cubical type theory.

[1] https://www.math-stockholm.se/en/kalender/maximilian-dore-algorithmically-finding-cells-in-kan-cubical-sets-1.1232953)
[2] https://arxiv.org/abs/2402.12169v1
[3] https://arxiv.org/abs/2402.12169v2