期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2020
卷号：2020
页码：1-26
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：The partial string avoidability problem is stated as follows: given a finite set of strings with possible “holes” (wildcard symbols), determine whether there exists a two-sided infinite string containing no substrings from this set, assuming that a hole matches every symbol. The problem is known to be NP-hard and in PSPACE, and this paper establishes its PSPACE-completeness. Next, string avoidability over the binary alphabet is interpreted as a version of conjunctive normal form satisfiability problem (SAT), where each clause has infinitely many shifted variants. Non-satisfiability of these formulas can be proved using variants of classical propositional proof systems, augmented with derivation rules for shifting proof lines (such as clauses, inequalities, polynomials, etc). First, it is proved that there is a particular formula that has a short refutation in Resolution with a shift rule, but requires classical proofs of exponential size At the same time, it is shown that exponential lower bounds for classical proof systems can be translated for their shifted versions. Finally, it is shown that superpolynomial lower bounds on the size of shifted proofs would separate NP from PSPACE; a connection to lower bounds on circuit complexity is also established.
