TY - JOUR

T1 - Computational and Proof Complexity of Partial String Avoidability

AU - Itsykson, Dmitry

AU - Okhotin, Alexander

AU - Oparin, Vsevolod

N1 - Publisher Copyright: © 2021 ACM.

PY - 2021/3

Y1 - 2021/3

N2 - 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 article establishes its PSPACE-completeness. Next, string avoidability over the binary alphabet is interpreted as a version of conjunctive normal form satisfiability problem, 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.

AB - 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 article establishes its PSPACE-completeness. Next, string avoidability over the binary alphabet is interpreted as a version of conjunctive normal form satisfiability problem, 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.

KW - avoidability

KW - lower bound

KW - Partial strings

KW - partial words

KW - proof complexity

KW - PSPACE-completeness

KW - LOWER BOUNDS

KW - RESOLUTION

KW - POLYNOMIAL CALCULUS

UR - http://www.scopus.com/inward/record.url?scp=85102980148&partnerID=8YFLogxK

UR - https://www.mendeley.com/catalogue/82e3eaca-6802-3831-937d-eb65fc6a7b6a/

U2 - 10.1145/3442365

DO - 10.1145/3442365

M3 - Article

AN - SCOPUS:85102980148

VL - 13

JO - ACM Transactions on Computation Theory

JF - ACM Transactions on Computation Theory

SN - 1942-3454

IS - 1

M1 - 3442365

ER -