Document Open Access Logo

Computational and Proof Complexity of Partial String Avoidability

Authors Dmitry Itsykson, Alexander Okhotin, Vsevolod Oparin

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2016.51.pdf
  • Filesize: 433 kB
  • 13 pages

Document Identifiers

Author Details

Dmitry Itsykson
Alexander Okhotin
Vsevolod Oparin

Cite As Get BibTex

Dmitry Itsykson, Alexander Okhotin, and Vsevolod Oparin. Computational and Proof Complexity of Partial String Avoidability. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 51:1-51:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.MFCS.2016.51

Abstract

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.

Subject Classification

Keywords
  • partial strings
  • partial words
  • avoidability
  • proof complexity
  • PSPACE-completeness

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Alfred V. Aho and Margaret J. Corasick. Efficient string matching: An aid to bibliographic search. Commun. ACM, 18(6):333-340, June 1975. Google Scholar
  2. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, pages 154-169, 2014. Google Scholar
  3. Olaf Beyersdorff, Leroy Chew, and Mikolas Janota. On unification of QBF resolution-based calculi. In Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part II, pages 81-93, 2014. Google Scholar
  4. Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. Proof complexity of resolution-based QBF calculi. In 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, March 4-7, 2015, Garching, Germany, pages 76-89, 2015. Google Scholar
  5. Brandon Blakeley, Francine Blanchet-Sadri, Josh Gunter, and Narad Rampersad. On the complexity of deciding avoidability of sets of partial words. Theor. Comput. Sci., 411(49):4263-4271, 2010. Google Scholar
  6. Francine Blanchet-Sadri, Raphaël M. Jungers, and Justin Palumbo. Testing avoidability on sets of partial words is hard. Theor. Comput. Sci., 410(8-10):968-972, 2009. Google Scholar
  7. Samuel R. Buss. Towards NP-P via proof complexity and search. Ann. Pure Appl. Logic, 163(7):906-917, 2012. Google Scholar
  8. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, March 1979. Google Scholar
  9. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39:297-308, 1985. Google Scholar
  10. Russell Impagliazzo, Pavel Pudlák, and Jirí Sgall. Lower bounds for the polynomial calculus and the gröbner basis algorithm. Computational Complexity, 8(2):127-144, 1999. Google Scholar
  11. Mikolás Janota and Joao Marques-Silva. Expansion-based QBF solving versus q-resolution. Theor. Comput. Sci., 577:25-42, 2015. Google Scholar
  12. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified boolean formulas. Inf. Comput., 117(1):12-18, 1995. Google Scholar
  13. M. Lothaire. Algebraic Combinatorics on Words. Cambridge University Press, 2002. Cambridge Books Online. Google Scholar
  14. Pavel Pudlak. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic, 62(3):981-998, 1997. Google Scholar
  15. Alexander A. Razborov. Lower bounds for the polynomial calculus. Computational Complexity, 7(4):291-324, 1998. Google Scholar
  16. Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209-219, 1987. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact