{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:19:19Z","timestamp":1750220359104,"version":"3.41.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2021,9,8]],"date-time":"2021-09-08T00:00:00Z","timestamp":1631059200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100006769","name":"Russian Science Foundation","doi-asserted-by":"crossref","award":["18-71-10042"],"award-info":[{"award-number":["18-71-10042"]}],"id":[{"id":"10.13039\/501100006769","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000893","name":"Simons Foundation","doi-asserted-by":"crossref","award":["578919"],"award-info":[{"award-number":["578919"]}],"id":[{"id":"10.13039\/100000893","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2021,10,31]]},"abstract":"<jats:p>This article is motivated by seeking lower bounds on OBDD(\u2227, w, r) refutations, namely, OBDD refutations that allow weakening and arbitrary reorderings. We first work with 1 - NBP \u2227 refutations based on read-once nondeterministic branching programs. These generalize OBDD(\u2227, r) refutations. There are polynomial size 1 - NBP(\u2227) refutations of the pigeonhole principle, hence 1-NBP(\u2227) is strictly stronger than OBDD}(\u2227, r). There are also formulas that have polynomial size tree-like resolution refutations but require exponential size 1-NBP(\u2227) refutations. As a corollary, OBDD}(\u2227, r) does not simulate tree-like resolution, answering a previously open question.<\/jats:p>\n          <jats:p>\n            The system 1-NBP(\u2227, \u2203) uses projection inferences instead of weakening. 1-NBP(\u2227, \u2203\n            <jats:sub>\n              <jats:italic>k<\/jats:italic>\n            <\/jats:sub>\n            is the system restricted to projection on at most\n            <jats:italic>k<\/jats:italic>\n            distinct variables. We construct explicit constant degree graphs\n            <jats:italic>G<\/jats:italic>\n            <jats:sub>\n              <jats:italic>n<\/jats:italic>\n            <\/jats:sub>\n            on\n            <jats:italic>n<\/jats:italic>\n            vertices and an \u03b5 &gt; 0, such that 1-NBP(\u2227, \u2203\n            <jats:sub>\n              \u03b5\n              <jats:italic>n<\/jats:italic>\n            <\/jats:sub>\n            ) refutations of the Tseitin formula for\n            <jats:italic>G<\/jats:italic>\n            <jats:sub>\n              <jats:italic>n<\/jats:italic>\n            <\/jats:sub>\n            require exponential size.\n          <\/jats:p>\n          <jats:p>\n            Second, we study the proof system OBDD}(\u2227, w, r\n            <jats:sub>\u2113<\/jats:sub>\n            ), which allows \u2113 different variable orders in a refutation. We prove an exponential lower bound on the complexity of tree-like OBDD(\u2227, w, r\n            <jats:sub>\u2113<\/jats:sub>\n            ) refutations for \u2113 = \u03b5 log\n            <jats:italic>n<\/jats:italic>\n            , where\n            <jats:italic>n<\/jats:italic>\n            is the number of variables and \u03b5 &gt; 0 is a constant. The lower bound is based on multiparty communication complexity.\n          <\/jats:p>","DOI":"10.1145\/3468855","type":"journal-article","created":{"date-parts":[[2021,9,8]],"date-time":"2021-09-08T19:02:44Z","timestamp":1631127764000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Lower Bounds on OBDD Proofs with Several Orders"],"prefix":"10.1145","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3837-334X","authenticated-orcid":false,"given":"Sam","family":"Buss","sequence":"first","affiliation":[{"name":"Department of Mathematics, University of California, San Diego, La Jolla, California, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2680-4800","authenticated-orcid":false,"given":"Dmitry","family":"Itsykson","sequence":"additional","affiliation":[{"name":"St. Petersburg Department of Steklov Institute of Mathematics of theRussian Academy of Sciences, Fontanka, St. Petersburg, Russia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Knop","sequence":"additional","affiliation":[{"name":"Department of Mathematics, University of California, San Diego, La Jolla, California, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Artur","family":"Riazanov","sequence":"additional","affiliation":[{"name":"St. Petersburg Department of Steklov Institute of Mathematics of theRussian Academy of Sciences, Fontanka, St. Petersburg, Russia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dmitry","family":"Sokolov","sequence":"additional","affiliation":[{"name":"St. Petersburg State University, Russia and St. Petersburg Department of Steklov Institute of Mathematics of the Russian Academy of Sciences, Fontanka, St. Petersburg, Russia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,9,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02579166"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.disc.2006.03.025"},{"key":"e_1_2_1_3_1","volume-title":"Spencer","author":"Alon Noga","year":"2000","unstructured":"Noga Alon and Joel H . Spencer . 2000 . The Probabilistic Method, 2 nd ed. Wiley Publishing . Noga Alon and Joel H. Spencer. 2000. The Probabilistic Method, 2nd ed. Wiley Publishing.","edition":"2"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804090"},{"volume-title":"Proceedings of the 10th International Conf. on Principles and Practice of Constraint Programming (Lecture Notes in Computer Science 3258)","author":"Atserias Albert","key":"e_1_2_1_5_1","unstructured":"Albert Atserias , Phokion G. Kolaitis , and Moshe Y. Vardi . 2004. Constraint propogation as a proof system . In Proceedings of the 10th International Conf. on Principles and Practice of Constraint Programming (Lecture Notes in Computer Science 3258) . Springer Verlag, 77\u201391. Albert Atserias, Phokion G. Kolaitis, and Moshe Y. Vardi. 2004. Constraint propogation as a proof system. In Proceedings of the 10th International Conf. on Principles and Practice of Constraint Programming (Lecture Notes in Computer Science 3258). Springer Verlag, 77\u201391."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/3235586.3235602"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90044-8"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2009.01.006"},{"volume-title":"Proceedings of the 6th Annual ACM Symposium on the Theory of Computing. 135\u2013148","author":"Stephen","key":"e_1_2_1_12_1","unstructured":"Stephen A. Cook and Robert A. Reckhow. 1974. On the lengths of proofs in the propositional calculus, preliminary version . In Proceedings of the 6th Annual ACM Symposium on the Theory of Computing. 135\u2013148 . Stephen A. Cook and Robert A. Reckhow. 1974. On the lengths of proofs in the propositional calculus, preliminary version. In Proceedings of the 6th Annual ACM Symposium on the Theory of Computing. 135\u2013148."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38536-0_11"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3188745.3188838"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS\u201917)","author":"Glinskih Ludmila","year":"2017","unstructured":"Ludmila Glinskih and Dmitry Itsykson . 2017 . Satisfiable Tseitin formulas are hard for nondeterministic read-once branching programs . In Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS\u201917) . 26:1\u201326:12. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2017.26 10.4230\/LIPIcs.MFCS.2017.26 Ludmila Glinskih and Dmitry Itsykson. 2017. Satisfiable Tseitin formulas are hard for nondeterministic read-once branching programs. In Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS\u201917). 26:1\u201326:12. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2017.26"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1137\/16M1082007"},{"volume-title":"Proceedings of the 19th Symposium on Theoretical Aspects of Computer Science (STACS\u201902)","author":"Grigoriev Dima","key":"e_1_2_1_18_1","unstructured":"Dima Grigoriev , Edward A. Hirsch , and Dmitrii V. Pasechnik . 2002. Complexity of semi-algebraic proofs . In Proceedings of the 19th Symposium on Theoretical Aspects of Computer Science (STACS\u201902) (Lecture Notes in Computer Science 2285). Springer Verlag, 419\u2013430. Dima Grigoriev, Edward A. Hirsch, and Dmitrii V. Pasechnik. 2002. Complexity of semi-algebraic proofs. In Proceedings of the 19th Symposium on Theoretical Aspects of Computer Science (STACS\u201902) (Lecture Notes in Computer Science 2285). Springer Verlag, 419\u2013430."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/jsl.2019.53"},{"key":"e_1_2_1_21_1","series-title":"Lecture Notes in Computer Science 6876","volume-title":"Proceedings of the Principles and Practice of Constraint Programming (CP\u201911)","author":"J\u00e4rvisalo Matti","unstructured":"Matti J\u00e4rvisalo . 2011. On the relative efficiency of DPLL and OBDDs with Axiom and Join . In Proceedings of the Principles and Practice of Constraint Programming (CP\u201911) ( Lecture Notes in Computer Science 6876 ) . Springer Verlag , 429\u2013437. DOI:https:\/\/doi.org\/10.1007\/978-3-642-23786-7_33 10.1007\/978-3-642-23786-7_33 Matti J\u00e4rvisalo. 2011. On the relative efficiency of DPLL and OBDDs with Axiom and Join. In Proceedings of the Principles and Practice of Constraint Programming (CP\u201911) (Lecture Notes in Computer Science 6876). Springer Verlag, 429\u2013437. DOI:https:\/\/doi.org\/10.1007\/978-3-642-23786-7_33"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1208358751"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02126799"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/552553"},{"key":"e_1_2_1_26_1","first-page":"1","article-title":"Symbolic techniques in satisfiability solving","volume":"35","author":"Pan Guoqiang","year":"2005","unstructured":"Guoqiang Pan and Moshe Y. Vardi . 2005 . Symbolic techniques in satisfiability solving . J. Autom. Reason. 35 , 1 \u2013 3 (2005), 25\u201350. DOI:https:\/\/doi.org\/10.1007\/s10817-005-9009-7 10.1007\/s10817-005-9009-7 Guoqiang Pan and Moshe Y. Vardi. 2005. Symbolic techniques in satisfiability solving. J. Autom. Reason. 35, 1\u20133 (2005), 25\u201350. DOI:https:\/\/doi.org\/10.1007\/s10817-005-9009-7","journal-title":"J. Autom. Reason."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275583"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/2833227.2833232"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/CCC.2008.34"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629334"},{"volume-title":"Automation of Reasoning. Vols. 1&2","author":"Siekmann Jorg","key":"e_1_2_1_32_1","unstructured":"Jorg Siekmann and Graham Wrightson . 1983. Automation of Reasoning. Vols. 1&2 . Springer-Verlag , Berlin . Jorg Siekmann and Graham Wrightson. 1983. Automation of Reasoning. Vols. 1&2. Springer-Verlag, Berlin."},{"key":"e_1_2_1_33_1","first-page":"115","article-title":"On the complexity of derivation in propositional logic","volume":"2","author":"Tsejtin G. S.","year":"1968","unstructured":"G. S. Tsejtin . 1968 . On the complexity of derivation in propositional logic . Studies in Constructive Mathematics and Mathematical Logic 2 (1968), 115 \u2013 125 . Reprinted in Reference [32, vol. 2], pp. 466-483. G. S. Tsejtin. 1968. On the complexity of derivation in propositional logic. Studies in Constructive Mathematics and Mathematical Logic 2 (1968), 115\u2013125. Reprinted in Reference [32, vol. 2], pp. 466-483.","journal-title":"Studies in Constructive Mathematics and Mathematical Logic"},{"key":"e_1_2_1_34_1","first-page":"107","article-title":"The factorization of linear graphs. J. London","volume":"2","author":"Tutte William T.","year":"1947","unstructured":"William T. Tutte . 1947 . The factorization of linear graphs. J. London Math. Soc. s1-22 , 2 (1947), 107 \u2013 111 . DOI:https:\/\/doi.org\/10.1112\/jlms\/s1-22.2.107 10.1112\/jlms William T. Tutte. 1947. The factorization of linear graphs. J. London Math. Soc. s1-22, 2 (1947), 107\u2013111. DOI:https:\/\/doi.org\/10.1112\/jlms\/s1-22.2.107","journal-title":"Math. Soc. s1-22"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190074"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/7531.8928"},{"key":"e_1_2_1_37_1","unstructured":"Ingo Wegener. 1987. Branching Programs and Binary Decision Diagrams: Theory and Applications. SIAM.  Ingo Wegener. 1987. Branching Programs and Binary Decision Diagrams: Theory and Applications. SIAM."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3468855","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3468855","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:21Z","timestamp":1750191441000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3468855"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,8]]},"references-count":35,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,10,31]]}},"alternative-id":["10.1145\/3468855"],"URL":"https:\/\/doi.org\/10.1145\/3468855","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2021,9,8]]},"assertion":[{"value":"2020-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-09-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}