Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

Computational and Proof Complexity of Partial String Avoidability

Computational and Proof Complexity of Partial String Avoidability 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. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png ACM Transactions on Computation Theory (TOCT) Association for Computing Machinery

Computational and Proof Complexity of Partial String Avoidability

Download PDF
25 pages

Loading next page...
 
/lp/association-for-computing-machinery/computational-and-proof-complexity-of-partial-string-avoidability-m0gIAgmw6U
Publisher
Association for Computing Machinery
Copyright
Copyright © 2021 ACM
ISSN
1942-3454
eISSN
1942-3462
DOI
10.1145/3442365
Publisher site
See Article on Publisher Site

Abstract

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.

Journal

ACM Transactions on Computation Theory (TOCT) – Association for Computing Machinery

Published: Jan 21, 2021

Keywords: PSPACE-completeness

References

  • Efficient string matching: An aid to bibliographic search
    Aho, Alfred V.; Corasick, Margaret J.
  • Lower bounds for polynomial calculus: Non-binomial case
    Alekhnovich, Michael; Razborov, Alexander A.
  • QBF resolution systems and their proof complexities
    Balabanov, Valeriy; Widl, Magdalena; Jiang, Jie-Hong R.
  • Finite and infinite words
    Berstel, J.; Perrin, D.
  • New resolution-based QBF calculi and their proof complexity
    Beyersdorff, Olaf; Chew, Leroy; Janota, Mikolás
  • Reasons for hardness in QBF proof systems
    Beyersdorff, Olaf; Hinde, Luke; Pich, Ján
  • On the complexity of deciding avoidability of sets of partial words
    Blakeley, Brandon; Blanchet-Sadri, Francine; Gunter, Josh; Rampersad, Narad
  • Testing avoidability on sets of partial words is hard
    Blanchet-Sadri, Francine; Jungers, Raphaël M.; Palumbo, Justin
  • Towards NP-P via proof complexity and search
    Buss, Samuel R.
  • The relative efficiency of propositional proof systems
    Cook, Stephen A.; Reckhow, Robert A.
  • The intractability of resolution
    Haken, Armin
  • Lower bounds for the polynomial calculus and the Gröbner basis algorithm
    Impagliazzo, Russell; Pudlák, Pavel; Sgall, Jirí
  • Expansion-based QBF solving versus Q-resolution
    Janota, Mikolás; Marques-Silva, Joao
  • Resolution for quantified Boolean formulas
    Büning, Hans Kleine; Karpinski, Marek; Flögel, Andreas
  • Search problems in the decision tree model
    Lovász, László; Naor, Moni; Newman, Ilan; Wigderson, Avi
  • Lower bounds for resolution and cutting plane proofs and monotone computations
    Pudlak, Pavel
  • Lower bounds for the polynomial calculus
    Razborov, Alexander A.
  • Hard examples for resolution
    Urquhart, Alasdair