{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:21:48Z","timestamp":1750220508148,"version":"3.41.0"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2021,1,21]],"date-time":"2021-01-21T00:00:00Z","timestamp":1611187200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100009409","name":"Russian Science Support Foundation","doi-asserted-by":"crossref","award":["16-11-10123"],"award-info":[{"award-number":["16-11-10123"]}],"id":[{"id":"10.13039\/100009409","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Theory"],"published-print":{"date-parts":[[2021,3,31]]},"abstract":"<jats:p>The partial string avoidability problem is stated as follows: given a finite set of strings with possible \u201choles\u201d (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.<\/jats:p>","DOI":"10.1145\/3442365","type":"journal-article","created":{"date-parts":[[2021,1,21]],"date-time":"2021-01-21T11:11:18Z","timestamp":1611227478000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Computational and Proof Complexity of Partial String Avoidability"],"prefix":"10.1145","volume":"13","author":[{"given":"Dmitry","family":"Itsykson","sequence":"first","affiliation":[{"name":"Steklov Institute of Mathematics at St.\u00a0Petersburg, St.\u00a0Petersburg, Russia"}]},{"given":"Alexander","family":"Okhotin","sequence":"additional","affiliation":[{"name":"St.\u00a0Petersburg State University, St. Petersburg, Russia"}]},{"given":"Vsevolod","family":"Oparin","sequence":"additional","affiliation":[{"name":"Facebook, Inc., CA, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,1,21]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/360825.360855"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.2001.959893"},{"volume-title":"Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201914)","author":"Balabanov Valeriy","key":"e_1_2_1_3_1","unstructured":"Valeriy Balabanov , Magdalena Widl , and Jie-Hong R. Jiang . 2014. QBF resolution systems and their proof complexities . In Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201914) . Springer, Cham, 154--169. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. 2014. QBF resolution systems and their proof complexities. In Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201914). Springer, Cham, 154--169."},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"J. Berstel and D. Perrin. 2002. Finite and infinite words. In Algebraic Combinatorics on Words M. Lothaire (Ed.). Cambridge University Press Cambridge 1--44.  J. Berstel and D. Perrin. 2002. Finite and infinite words. In Algebraic Combinatorics on Words M. Lothaire (Ed.). Cambridge University Press Cambridge 1--44.","DOI":"10.1017\/CBO9781107326019.002"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352155"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2017.14"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.006"},{"key":"e_1_2_1_8_1","first-page":"8","article-title":"Testing avoidability on sets of partial words is hard","volume":"410","author":"Blanchet-Sadri Francine","year":"2009","unstructured":"Francine Blanchet-Sadri , Rapha\u00ebl M. Jungers , and Justin Palumbo . 2009 . Testing avoidability on sets of partial words is hard . Theor. Comput. Sci. 410 , 8 \u2013 10 (2009), 968--972. Francine Blanchet-Sadri, Rapha\u00ebl M. Jungers, and Justin Palumbo. 2009. Testing avoidability on sets of partial words is hard. Theor. Comput. Sci. 410, 8\u201310 (2009), 968--972.","journal-title":"Theor. Comput. Sci."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.009"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050024"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.01.048"},{"key":"e_1_2_1_14_1","first-page":"12","article-title":"Resolution for quantified Boolean formulas. Info","volume":"117","author":"B\u00fcning Hans Kleine","year":"1995","unstructured":"Hans Kleine B\u00fcning , Marek Karpinski , and Andreas Fl\u00f6gel . 1995 . Resolution for quantified Boolean formulas. Info . Comput. 117 , 1 (1995), 12 -- 18 . Hans Kleine B\u00fcning, Marek Karpinski, and Andreas Fl\u00f6gel. 1995. Resolution for quantified Boolean formulas. Info. Comput. 117, 1 (1995), 12--18.","journal-title":"Comput."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0895480192233867"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275583"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050013"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/7531.8928"}],"container-title":["ACM Transactions on Computation Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3442365","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3442365","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:21Z","timestamp":1750195461000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3442365"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,21]]},"references-count":18,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,3,31]]}},"alternative-id":["10.1145\/3442365"],"URL":"https:\/\/doi.org\/10.1145\/3442365","relation":{},"ISSN":["1942-3454","1942-3462"],"issn-type":[{"type":"print","value":"1942-3454"},{"type":"electronic","value":"1942-3462"}],"subject":[],"published":{"date-parts":[[2021,1,21]]},"assertion":[{"value":"2020-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-01-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}