{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T18:32:55Z","timestamp":1743013975060,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030510732"},{"type":"electronic","value":"9783030510749"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"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":[[2020]]},"DOI":"10.1007\/978-3-030-51074-9_3","type":"book-chapter","created":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T22:02:47Z","timestamp":1593468167000},"page":"32-47","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Covered Clauses Are Not Propagation Redundant"],"prefix":"10.1007","author":[{"given":"Lee A.","family":"Barnett","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Cerna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,6,24]]},"reference":[{"issue":"4","key":"3_CR1","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/BF01302964","volume":"14","author":"M Ajtai","year":"1994","unstructured":"Ajtai, M.: The complexity of the pigeonhole principle. Combinatorica 14(4), 417\u2013433 (1994)","journal-title":"Combinatorica"},{"key":"3_CR2","unstructured":"Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT entering the SAT competition 2018. In: Heule, M.J.H., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2018, pp. 13\u201314. Department of Computer Science Series of Publications B, University of Helsinki (2018)"},{"key":"3_CR3","unstructured":"Biere, A.: CaDiCaL at the SAT race 2019. In: Heule, M.J.H., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of SAT Race 2019, pp. 8\u20139. Department of Computer Science Series of Publications B, University of Helsinki (2019)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-030-24258-9_5","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"S Buss","year":"2019","unstructured":"Buss, S., Thapen, N.: DRAT proofs, propagation redundancy, and extended resolution. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 71\u201389. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_5"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/3-540-16486-3_93","volume-title":"Structure in Complexity Theory","author":"JY Cai","year":"1986","unstructured":"Cai, J.Y., Hemachandra, L.: The Boolean hierarchy: hardware over NP. In: Selman, A.L. (ed.) Structure in Complexity Theory. LNCS, vol. 223, pp. 105\u2013124. Springer, Heidelberg (1986). https:\/\/doi.org\/10.1007\/3-540-16486-3_93"},{"issue":"1","key":"3_CR6","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-030-24258-9_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"K Fazekas","year":"2019","unstructured":"Fazekas, K., Biere, A., Scholl, C.: Incremental inprocessing in SAT solving. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 136\u2013154. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_9"},{"key":"3_CR8","unstructured":"Gableske, O.: BossLS preprocessing and stochastic local search. In: Balint, A., Belov, A., Diepold, D., Gerber, S., J\u00e4rvisalo, M., Sinz, C. (eds.) Proceedings of SAT Challenge 2012, pp. 10\u201311. Department of Computer Science Series of Publications B, University of Helsinki (2012)"},{"issue":"2\u20133","key":"3_CR9","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39(2\u20133), 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H.: Schur number five. In: Proceedings of the 32nd AAAI Conference on Artificial Intelligence (AAAI 2018), pp. 6598\u20136606 (2018)","DOI":"10.1609\/aaai.v32i1.12209"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-319-89963-3_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MJH Heule","year":"2018","unstructured":"Heule, M.J.H., Biere, A.: What a difference a variable makes. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 75\u201392. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_5"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Clause elimination procedures for CNF formulas. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 357\u2013371. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16242-8_26","DOI":"10.1007\/978-3-642-16242-8_26"},{"key":"3_CR13","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Covered clause elimination. In: Voronkov, A., Sutcliffe, G., Baaz, M., Ferm\u00fcller, C. (eds.) Logic for Programming, Artificial Intelligence and Reasoning - LPAR 17 (short paper). EPiC Series in Computing, vol. 13, pp. 41\u201346. EasyChair (2010)"},{"issue":"1","key":"3_CR14","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1613\/jair.4694","volume":"53","author":"MJH Heule","year":"2015","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intell. Res. 53(1), 127\u2013168 (2015)","journal-title":"J. Artif. Intell. Res."},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-63046-5_9","volume-title":"Automated Deduction \u2013 CADE 26","author":"MJH Heule","year":"2017","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 130\u2013147. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_9"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-030-17462-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MJH Heule","year":"2019","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Encoding redundancy for satisfaction-driven clause learning. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 41\u201358. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_3"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/s10817-019-09516-0","volume":"64","author":"MJH Heule","year":"2020","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Strong extension-free proof systems. J. Autom. Reason. 64, 533\u2013554 (2020)","journal-title":"J. Autom. Reason."},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-319-70389-3_12","volume-title":"Hardware and Software: Verification and Testing","author":"MJH Heule","year":"2017","unstructured":"Heule, M.J.H., Kiesl, B., Seidl, M., Biere, A.: PRuning through satisfaction. In: Strichman, O., Tzoref-Brill, R. (eds.) HVC 2017. LNCS, vol. 10629, pp. 179\u2013194. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_12"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MJH Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via Cube-and-Conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_15"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-12002-2_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129\u2013144. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_10"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_28"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-030-31784-3_3","volume-title":"Automated Technology for Verification and Analysis","author":"B Kiesl","year":"2019","unstructured":"Kiesl, B., Heule, M.J.H., Biere, A.: Truth assignments as conditional autarkies. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 48\u201364. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_3"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-319-40229-1_5","volume-title":"Automated Reasoning","author":"B Kiesl","year":"2016","unstructured":"Kiesl, B., Seidl, M., Tompits, H., Biere, A.: Super-blocked clauses. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 45\u201361. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_5"},{"key":"3_CR24","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.artint.2015.03.004","volume":"224","author":"B Konev","year":"2015","unstructured":"Konev, B., Lisitsa, A.: Computer-aided proof of Erd\u0151s discrepancy properties. Artif. Intell. 224, 103\u2013118 (2015)","journal-title":"Artif. Intell."},{"issue":"97","key":"3_CR25","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96","author":"O Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discret. Appl. Math. 96(97), 149\u2013176 (1999)","journal-title":"Discret. Appl. Math."},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-31612-8_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"N Manthey","year":"2012","unstructured":"Manthey, N.: Coprocessor 2.0 \u2013 a flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 436\u2013441. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_34"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/11814948_13","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"I Mironov","year":"2006","unstructured":"Mironov, I., Zhang, L.: Applications of SAT solvers to cryptanalysis of hash functions. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 102\u2013115. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_13"},{"issue":"2","key":"3_CR28","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1016\/0022-0000(84)90068-0","volume":"28","author":"C Papadimitriou","year":"1984","unstructured":"Papadimitriou, C., Yannakakis, M.: The complexity of facets (and some facets of complexity). J. Comput. Syst. Sci. 28(2), 244\u2013259 (1984)","journal-title":"J. Comput. Syst. Sci."},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/BFb0028832","volume-title":"Fundamentals of Computation Theory","author":"G Wechsung","year":"1985","unstructured":"Wechsung, G.: On the Boolean closure of NP. In: Budach, L. (ed.) FCT 1985. LNCS, vol. 199, pp. 485\u2013493. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/BFb0028832"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-51074-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,2]],"date-time":"2022-07-02T21:32:40Z","timestamp":1656797560000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-51074-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030510732","9783030510749"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-51074-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"24 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ijcar2020.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"150","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.03","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7.38","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11 system descriptions are also included. The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}