Towards Understanding Satisfiability, Group Isomorphism and Their Connections
Bangsheng Tang · 2013
This work studies two of the most fundamental problems in computer science: satisfiability (SAT), and group isomorphism (GroupISO). We propose new approaches and concepts, introduce new techniques and we identify connections between these two problems. For SAT, our study focuses on exact algorithms. First, we investigate the performance of the current world record algorithm for general SAT, and show new lower bounds, introducing a new expansion property. We also conduct comprehensive research on practical instances parameterized by tree-width or path-width w. We give optimal, modulo our technique, optimal algorithms, new characterizations of small space computation using SAT of bounded width parameters, and propose a conjecture regarding lower bounds for time-space trade-o↵s. Specifically, Alekhnovitch and Razborov in 2002 gave an algorithm whose running time is 2wnO(1) and space 2wnO(1) and asked if anything can be done to reduce the space to polynomial. We give an algorithm that runs in time 2logn·wnO(1) and space nO(1), and we conjecture that removing the log n without blowing up the running space to exponential in w is impossible and show that the conjecture is closely related to the question of “NC vs SC”. In the setting of propositional proof complexity, we make progress in validating our conjecture by lifting a previous trade-o↵ lower bound result for resolution by Beam, Beck and Impagliazzo to the stronger polynomial calculus resolution. We bring tools developed in our study of SAT toGroupISO and obtain the following two results. First, we observe that GroupISO can be encoded as SAT instances of small width parameters by showing a nondeterministic algorithm which runs simultaneously in time nO(1) and space O(log2 n), where n is the number of group elements. Second, we compare the complexity of GroupISO and the well-known graph isomorphism problem (GraphISO), and give a new conditional separation. In an independent direction, we introduce a family of small-space heuristics. Finally, for GroupISO with the promise that the input groups are from a certain class, we extend the borderline of polynomial time tractable to groups with normal Hall subgroups and introduce techniques from representation theory into group isomorphism testing.