{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T18:42:45Z","timestamp":1661971365349},"reference-count":40,"publisher":"Society for Industrial & Applied Mathematics (SIAM)","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SIAM J. Comput."],"published-print":{"date-parts":[[2022,8]]},"DOI":"10.1137\/20m1362528","type":"journal-article","created":{"date-parts":[[2022,8,23]],"date-time":"2022-08-23T16:09:37Z","timestamp":1661270977000},"page":"1368-1399","source":"Crossref","is-referenced-by-count":0,"title":["On CDCL-Based Proof Systems with the Ordered Decision Strategy"],"prefix":"10.1137","volume":"51","author":[{"given":"Nathan","family":"Mull","sequence":"first","affiliation":[]},{"given":"Shuo","family":"Pang","sequence":"additional","affiliation":[]},{"given":"Alexander","family":"Razborov","sequence":"additional","affiliation":[]}],"member":"351","published-online":{"date-parts":[[2022,8,23]]},"reference":[{"key":"atypb1","first-page":"1167","volume-title":"International Workshop on Logic and Synthesis","author":"Aloul F. A.","year":"2001"},{"key":"atypb2","doi-asserted-by":"publisher","DOI":"10.1145\/764808.764839"},{"key":"atypb3","doi-asserted-by":"publisher","DOI":"10.1613\/jair.3152"},{"key":"atypb4","first-page":"399","volume-title":"IJCAI'09: Proceedings of the 21st International Joint Conference on Artificial Intelligence","author":"Audemard G.","year":"2009"},{"key":"atypb5","first-page":"203","volume-title":"AAAI'97\/IAAI'97: Proceedings of the 14th National Conference on Artificial Intelligence and 9th Conference on Innovative Applications of Artificial Intelligence, AAAI","author":"Bayardo R. J.","year":"1997"},{"key":"atypb6","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700369156"},{"key":"atypb7","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1410"},{"key":"atypb8","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v28i1.9121"},{"key":"atypb9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_4"},{"key":"atypb10","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"atypb11","first-page":"1","volume-title":"Proceedings of Pragmatics of SAT 2015 and 2018, Sixth Pragmatics of SAT Workshop, EasyChair","author":"Biere A.","year":"2015"},{"key":"atypb12","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA336"},{"key":"atypb13","unstructured":"A. Blake,Canonical Expressions in Boolean Algebra, Ph.D. thesis, University of Chicago, 1938."},{"key":"atypb14","doi-asserted-by":"publisher","DOI":"10.1051\/ita:1999108"},{"key":"atypb15","doi-asserted-by":"publisher","DOI":"10.1613\/jair.4260"},{"key":"atypb16","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799352474"},{"key":"atypb17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_3"},{"key":"atypb18","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(4:13)2008"},{"key":"atypb19","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(2:16)2014"},{"key":"atypb20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_10"},{"key":"atypb21","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"atypb22","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"atypb23","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"atypb24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_11"},{"key":"atypb25","doi-asserted-by":"publisher","DOI":"10.1007\/11757283_5"},{"key":"atypb26","first-page":"283","volume-title":"Proceedings of the 23rd AAAI Conference on Artificial Intelligence","author":"Hertel P.","year":"2008"},{"key":"atypb27","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.03.013"},{"key":"atypb28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51825-7_17"},{"key":"atypb29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26287-1_14"},{"key":"atypb30","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48159-1_5"},{"key":"atypb31","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"atypb32","volume-title":"Automated Theorem Proving Using SAT","author":"McGregor R. E.","year":"2011"},{"key":"atypb33","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"atypb34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51825-7_12"},{"key":"atypb35","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"atypb36","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(3:15)2013"},{"key":"atypb37","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2010.10.002"},{"key":"atypb38","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"atypb39","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_40"},{"key":"atypb40","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i02.5527"}],"container-title":["SIAM Journal on Computing"],"original-title":[],"language":"en","deposited":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T18:23:34Z","timestamp":1661970214000},"score":1,"resource":{"primary":{"URL":"https:\/\/epubs.siam.org\/doi\/10.1137\/20M1362528"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["10.1137\/20M1362528"],"URL":"https:\/\/doi.org\/10.1137\/20m1362528","relation":{},"ISSN":["0097-5397","1095-7111"],"issn-type":[{"value":"0097-5397","type":"print"},{"value":"1095-7111","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8]]}}}