{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:24:31Z","timestamp":1743063871295,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030802226"},{"type":"electronic","value":"9783030802233"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-80223-3_9","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"116-133","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Characterizing Tseitin-Formulas with Short Regular Resolution Refutations"],"prefix":"10.1007","author":[{"given":"Alexis","family":"de Colnet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Mengel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","unstructured":"Alekhnovich, M., Johannsen, J., Pitassi, T., Urquhart, A.: An exponential separation between regular and general resolution. Theory Comput. 3(1), 81\u2013102 (2007). https:\/\/doi.org\/10.4086\/toc.2007.v003a005","DOI":"10.4086\/toc.2007.v003a005"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Alekhnovich, M., Razborov, A.A.: Satisfiability, branch-width and tseitin tautologies. Comput. Complex. 20(4), 649\u2013678 (2011). https:\/\/doi.org\/10.1007\/s00037-011-0033-1","DOI":"10.1007\/s00037-011-0033-1"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Atserias, A., Bonacina, I., de Rezende, S.F., Lauria, M., Nordstr\u00f6m, J., Razborov, A.A.: Clique is hard on average for regular resolution. In: Diakonikolas, I., Kempe, D., Henzinger, M. (eds.) Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2018, Los Angeles, CA, USA, 25\u201329 June, 2018. pp. 866\u2013877. ACM (2018). https:\/\/doi.org\/10.1145\/3188745.3188856","DOI":"10.1145\/3188745.3188856"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Beame, P., Beck, C., Impagliazzo, R.: Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space. In: Karloff, H.J., Pitassi, T. (eds.) Proceedings of the 44th Symposium on Theory of Computing Conference, STOC 2012, New York, NY, USA, 19\u201322 May, 2012, pp. 213\u2013232. ACM (2012). https:\/\/doi.org\/10.1145\/2213977.2213999","DOI":"10.1145\/2213977.2213999"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Beck, C., Impagliazzo, R.: Strong ETH holds for regular resolution. In: Boneh, D., Roughgarden, T., Feigenbaum, J. (eds.) Symposium on Theory of Computing Conference, STOC 2013, Palo Alto, CA, USA, 1\u20134 June, 2013. pp. 487\u2013494. ACM (2013). https:\/\/doi.org\/10.1145\/2488608.2488669","DOI":"10.1145\/2488608.2488669"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Ben-Sasson, E.: Hard examples for the bounded depth frege proof system. Comput. Complex. 11(3-4), 109\u2013136 (2002). https:\/\/doi.org\/10.1007\/s00037-002-0172-5","DOI":"10.1007\/s00037-002-0172-5"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Bodlaender, H.L., Koster, A.M.C.A.: Safe separators for treewidth. Discret. Math. 306(3), 337\u2013350 (2006). https:\/\/doi.org\/10.1016\/j.disc.2005.12.017","DOI":"10.1016\/j.disc.2005.12.017"},{"key":"9_CR8","unstructured":"Bova, S., Capelli, F., Mengel, S., Slivovsky, F.: Knowledge compilation meets communication complexity. In: Kambhampati, S. (ed.) Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9\u201315 July 2016, pp. 1008\u20131014. IJCAI\/AAAI Press (2016). http:\/\/www.ijcai.org\/Abstract\/16\/147"},{"key":"9_CR9","unstructured":"Buss, S., Nordstr\u00f6m, J.: Proof complexity and sat solving. Chapter to appear in the 2nd edition of Handbook of Satisfiability, Draft version available at https:\/\/www.math.ucsd.edu\/~sbuss\/ResearchWeb\/ProofComplexitySAT (2019)"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Darwiche, A.: Decomposable negation normal form. J. ACM 48(4), 608\u2013647 (2001). https:\/\/doi.org\/10.1145\/502090.502091","DOI":"10.1145\/502090.502091"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. 17, 229\u2013264 (2002). https:\/\/doi.org\/10.1613\/jair.989","DOI":"10.1613\/jair.989"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962). https:\/\/doi.org\/10.1145\/368273.368557","DOI":"10.1145\/368273.368557"},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960). https:\/\/doi.org\/10.1145\/321033.321034","DOI":"10.1145\/321033.321034"},{"key":"9_CR14","doi-asserted-by":"publisher","unstructured":"Galesi, N., Itsykson, D., Riazanov, A., Sofronova, A.: Bounded-depth frege complexity of tseitin formulas for all graphs. In: Rossmanith, P., Heggernes, P., Katoen, J. (eds.) 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26\u201330, 2019, Aachen, Germany. LIPIcs, vol. 138, pp. 49:1\u201349:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2019.49","DOI":"10.4230\/LIPIcs.MFCS.2019.49"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Galesi, N., Talebanfard, N., Tor\u00e1n, J.: Cops-robber games and the resolution of tseitin formulas. ACM Trans. Comput. Theory 12(2), 9:1\u20139:22 (2020). https:\/\/doi.org\/10.1145\/3378667","DOI":"10.1145\/3378667"},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Glinskih, L., Itsykson, D.: Satisfiable tseitin formulas are hard for nondeterministic read-once branching programs. In: Larsen, K.G., Bodlaender, H.L., Raskin, J. (eds.) 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017, August 21\u201325, 2017 - Aalborg, Denmark. LIPIcs, vol. 83, pp. 26:1\u201326:12. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2017.26","DOI":"10.4230\/LIPIcs.MFCS.2017.26"},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"Goerdt, A.: Regular resolution versus unrestricted resolution. SIAM J. Comput. 22(4), 661\u2013683 (1993). https:\/\/doi.org\/10.1137\/0222044","DOI":"10.1137\/0222044"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Harvey, D.J., Wood, D.R.: Parameters tied to treewidth. J. Graph Theory 84(4), 364\u2013385 (2017). https:\/\/doi.org\/10.1002\/jgt.22030","DOI":"10.1002\/jgt.22030"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-38536-0_14","volume-title":"Computer Science \u2013 Theory and Applications","author":"D Itsykson","year":"2013","unstructured":"Itsykson, D., Oparin, V.: Graph expansion, tseitin formulas and resolution proofs for CSP. In: Bulatov, A.A., Shur, A.M. (eds.) CSR 2013. LNCS, vol. 7913, pp. 162\u2013173. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38536-0_14"},{"key":"9_CR20","unstructured":"Itsykson, D., Riazanov, A., Sagunov, D., Smirnov, P.: Almost tight lower bounds on regular resolution refutations of tseitin formulas for all constant-degree graphs. Electron. Colloquium Comput. Complex. 26, 178 (2019). https:\/\/eccc.weizmann.ac.il\/report\/2019\/178"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Lov\u00e1sz, L., Naor, M., Newman, I., Wigderson, A.: Search problems in the decision tree model. SIAM J. Discret. Math. 8(1), 119\u2013132 (1995). https:\/\/doi.org\/10.1137\/S0895480192233867","DOI":"10.1137\/S0895480192233867"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Nordstr\u00f6m, J.: On the interplay between proof complexity and SAT solving. ACM SIGLOG News 2(3), 19\u201344 (2015). https:\/\/dl.acm.org\/citation.cfm?id=2815497","DOI":"10.1145\/2815493.2815497"},{"key":"9_CR23","doi-asserted-by":"publisher","unstructured":"Razgon, I.: On the read-once property of branching programs and cnfs of bounded treewidth. Algorithmica 75(2), 277\u2013294 (2016). https:\/\/doi.org\/10.1007\/s00453-015-0059-x","DOI":"10.1007\/s00453-015-0059-x"},{"key":"9_CR24","first-page":"115","volume":"2","author":"G Tseitin","year":"1968","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. Stud. Constructive Math. Math. Logic Part 2, 115\u2013125 (1968)","journal-title":"Stud. Constructive Math. Math. Logic Part"},{"key":"9_CR25","doi-asserted-by":"publisher","unstructured":"Urquhart, A.: Hard examples for resolution. J. ACM 34(1), 209\u2013219 (1987). https:\/\/doi.org\/10.1145\/7531.8928","DOI":"10.1145\/7531.8928"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Urquhart, A.: A near-optimal separation of regular and general resolution. SIAM J. Comput. 40(1), 107\u2013121 (2011). https:\/\/doi.org\/10.1137\/090772897","DOI":"10.1137\/090772897"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-030-51825-7_14","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2020","author":"M Vinyals","year":"2020","unstructured":"Vinyals, M., Elffers, J., Johannsen, J., Nordstr\u00f6m, J.: Simplified and improved separations between regular and general resolution by lifting. In: Pulina, L., Seidl, M. (eds.) SAT 2020. LNCS, vol. 12178, pp. 182\u2013200. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_14"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-80223-3_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T23:31:25Z","timestamp":1625182285000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Barcelona","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.iiia.csic.es\/sat2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}