TY - GEN

T1 - Computational and proof complexity of partial string avoidability

AU - Itsykson, Dmitry

AU - Okhotin, Alexander

AU - Oparin, Vsevolod

PY - 2016/8/1

Y1 - 2016/8/1

N2 - The partial string avoidability problem, also known as partial word avoidability, is stated as follows: Given a finite set of strings with possible "holes" (undefined symbols), determine whether there exists any 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 (CNF) satisfiability problem (SAT), with each clause having 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 constraints (such as clauses, inequalities, polynomials, etc). Two results on their proof complexity are established. First, there is a particular formula that has a short refutation in Resolution with shift, but requires classical proofs of exponential size (Resolution, Cutting Plane, Polynomial Calculus, etc.). At the same time, exponential lower bounds for shifted versions of classical proof systems are established.

AB - The partial string avoidability problem, also known as partial word avoidability, is stated as follows: Given a finite set of strings with possible "holes" (undefined symbols), determine whether there exists any 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 (CNF) satisfiability problem (SAT), with each clause having 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 constraints (such as clauses, inequalities, polynomials, etc). Two results on their proof complexity are established. First, there is a particular formula that has a short refutation in Resolution with shift, but requires classical proofs of exponential size (Resolution, Cutting Plane, Polynomial Calculus, etc.). At the same time, exponential lower bounds for shifted versions of classical proof systems are established.

KW - Avoidability

KW - Partial strings

KW - Partial words

KW - Proof complexity

KW - PSPACEcompleteness

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

U2 - 10.4230/LIPIcs.MFCS.2016.51

DO - 10.4230/LIPIcs.MFCS.2016.51

M3 - Conference contribution

AN - SCOPUS:85012915552

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 41st International Symposium on Mathematical Foundations of Computer Science, MFCS 2016

A2 - Muscholl, Anca

A2 - Faliszewski, Piotr

A2 - Niedermeier, Rolf

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 41st International Symposium on Mathematical Foundations of Computer Science, MFCS 2016

Y2 - 22 August 2016 through 26 August 2016

ER -