{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:59:18Z","timestamp":1759147158853},"reference-count":22,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":2202,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2008,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We prove an exponential lower bound on the size of proofs in the proof system operating with ordered binary decision diagrams introduced by Atserias, Kolaitis and Vardi [2]. In fact, the lower bound applies to semantic derivations operating with sets defined by OBDDs. We do not assume any particular format of proofs or ordering of variables, the hard formulas are in CNF. We utilize (somewhat indirectly) feasible interpolation.<\/jats:p><jats:p>We define a proof system combining resolution and the OBDD proof system.<\/jats:p>","DOI":"10.2178\/jsl\/1208358751","type":"journal-article","created":{"date-parts":[[2008,10,14]],"date-time":"2008-10-14T15:19:02Z","timestamp":1223997542000},"page":"227-237","source":"Crossref","is-referenced-by-count":14,"title":["An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams"],"prefix":"10.1017","volume":"73","author":[{"given":"Jan","family":"Kraj\u00ed\u010dek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200004709_ref022","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898719789"},{"key":"S0022481200004709_ref017","unstructured":"Mikle-Bar\u00e1t O. , Strong proof systems, Master's thesis, Charles University, 2007, Available at the ECCC."},{"key":"S0022481200004709_ref016","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511574948"},{"key":"S0022481200004709_ref014","doi-asserted-by":"publisher","DOI":"10.4064\/fm170-1-8"},{"key":"S0022481200004709_ref011","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511529948"},{"key":"S0022481200004709_ref010","first-page":"73","volume":"59","author":"Kraj\u00ed\u010dek","year":"1994","journal-title":"Lower bounds to the size of constant-depth propositional proofs"},{"key":"S0022481200004709_ref008","first-page":"220","volume-title":"Logic in computer science","author":"Impagliazzo","year":"1994"},{"key":"S0022481200004709_ref007","volume-title":"Constraint processing","author":"Dechter","year":"2003"},{"key":"S0022481200004709_ref006","first-page":"36","volume":"44","author":"Cook","year":"1979","journal-title":"The relative efficiency of propositional proof systems"},{"key":"S0022481200004709_ref005","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"S0022481200004709_ref003","first-page":"708","author":"Bonet","year":"1997","journal-title":"Lower bounds for cutting planes proofs with small coefficients"},{"key":"S0022481200004709_ref018","first-page":"981","author":"Pudl\u00e1k","year":"1997","journal-title":"Lower bounds for resolution and cutting plane proofs and monotone computations"},{"key":"S0022481200004709_ref019","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)80023-2"},{"key":"S0022481200004709_ref012","first-page":"457","volume":"62","author":"Kraj\u00ed\u010dek","year":"1997","journal-title":"Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic"},{"key":"S0022481200004709_ref013","first-page":"1582","volume":"63","author":"Kraj\u00ed\u010dek","year":"1998","journal-title":"Discretely ordered modules as a first-order extension of the cutting planes proof system"},{"key":"S0022481200004709_ref004","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"S0022481200004709_ref020","first-page":"201","article-title":"Unprovability of lower bounds on the circuit size in certain fragments of bounded arithmetic","volume":"59","author":"Razborov","year":"1995","journal-title":"Izvestiya of the R.A.N."},{"key":"S0022481200004709_ref021","volume-title":"The complexity of Boolean functions","author":"Wegener","year":"1987"},{"key":"S0022481200004709_ref015","first-page":"82","volume-title":"Logic and computational complexity (Proc. of the meeting held in Indianapolis, October 1994)","volume":"140","author":"Kraj\u00ed\u010dek","year":"1998"},{"key":"S0022481200004709_ref009","unstructured":"Kraj\u00ed\u010dek J. , Propositional proof complexity I, lecture notes available at http:\/\/www.math.cas.cz\/~krajicek\/ds1.ps."},{"key":"S0022481200004709_ref002","first-page":"77","volume-title":"10th Int. Conf. on Principles and Practice of Constraint Programing","volume":"3258","author":"Atserias","year":"2004"},{"key":"S0022481200004709_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/BF02579196"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200004709","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T00:25:19Z","timestamp":1556670319000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200004709\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,3]]}},"alternative-id":["S0022481200004709"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1208358751","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,3]]}}}