{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:13:14Z","timestamp":1742911994092,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030518240"},{"type":"electronic","value":"9783030518257"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/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":"http:\/\/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-51825-7_1","type":"book-chapter","created":{"date-parts":[[2020,6,30]],"date-time":"2020-06-30T23:00:13Z","timestamp":1593558013000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Sorting Parity Encodings by Reusing Variables"],"prefix":"10.1007","author":[{"given":"Leroy","family":"Chew","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,6,26]]},"reference":[{"key":"1_CR1","unstructured":"Biere, A.: CaDiCaL at the SAT Race 2019 (2019)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Buss, S., Thapen, N.: DRAT proofs, propagation redundancy, and extended resolution. In: International Conference on Theory and Applications of Satisfiability Testing. pp. 71\u201389. Springer (2019)","DOI":"10.1007\/978-3-030-24258-9_5"},{"key":"1_CR3","unstructured":"Crawford, J.M., Kearns, M.J., Schapire, R.E.: The minimal disagreement parity problem as a hard satisfiability problem (1994)"},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7, 210\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Han, C.S., Jiang, J.H.R.: When Boolean satisfiability meets Gaussian elimination in a simplex way. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification. pp. 410\u2013426. Springer, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-31424-7_31"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Heule, M., van Maaren, H.: Aligning CNF- and equivalence-reasoning. In: Hoos, H.H., Mitchell, D.G. (eds.) Theory and Applications of Satisfiability Testing. pp. 145\u2013156. Springer, Berlin, Heidelberg (2005)","DOI":"10.1007\/11527695_12"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning. pp. 355\u2013370. Springer, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Kiesl, B., Rebola-Pardo, A., Heule, M.J.H.: Extended resolution simulates DRAT. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14\u201317, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10900, pp. 516\u2013531. Springer (2018)","DOI":"10.1007\/978-3-319-94205-6_34"},{"key":"1_CR9","unstructured":"Laitinen, T., Junttila, T., Niemel\u00e4, I.: Extending clause learning DPLL with parity reasoning. In: Proceedings of the 2010 Conference on ECAI 2010: 19th European Conference on Artificial Intelligence. pp. 21\u201326. IOS Press, NLD (2010)"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Laitinen, T., Junttila, T., Niemela, I.: Equivalence class based parity reasoning with DPLL(XOR). In: Proceedings of the 2011 IEEE 23rd International Conference on Tools with Artificial Intelligence. pp. 649\u2013658. ICTAI \u201911, IEEE Computer Society, USA (2011)","DOI":"10.1109\/ICTAI.2011.103"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Li, C.M.: Equivalent literal propagation in the DLL procedure. Discrete Applied Mathematics 130(2), 251\u2013276 (2003), the Renesse Issue on Satisfiability","DOI":"10.1016\/S0166-218X(02)00407-9"},{"key":"1_CR12","unstructured":"Marques Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability. IOS Press (2009)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Ostrowski, R., Gr\u00e9goire, \u00c9., Mazure, B., Sa\u00efs, L.: Recovering and exploiting structural knowledge from CNF formulas. In: Van Hentenryck, P. (ed.) Principles and Practice of Constraint Programming - CP 2002. pp. 185\u2013199. Springer, Berlin, Heidelberg (2002)","DOI":"10.1007\/3-540-46135-3_13"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Philipp, T., Rebola-Pardo, A.: DRAT proofs for XOR reasoning. In: Michael, L., Kakas, A. (eds.) Logics in Artificial Intelligence. pp. 415\u2013429. Springer International Publishing, Cham (2016)","DOI":"10.1007\/978-3-319-48758-8_27"},{"issue":"2","key":"1_CR15","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence 175(2), 512\u2013525 (2011)","journal-title":"Artificial Intelligence"},{"issue":"2","key":"1_CR16","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1145\/321160.321166","volume":"10","author":"JA Robinson","year":"1963","unstructured":"Robinson, J.A.: Theorem-proving on the computer. Journal of the ACM 10(2), 163\u2013174 (1963)","journal-title":"Journal of the ACM"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) Computer Science \u2013 Theory and Applications. pp. 600\u2013611. Springer, Berlin, Heidelberg (2006)","DOI":"10.1007\/11753728_60"},{"key":"1_CR18","unstructured":"Soos, M.: Enhanced Gaussian elimination in DPLL-based SAT solvers. In: Berre, D.L. (ed.) POS-10. Pragmatics of SAT. EPiC Series in Computing, vol. 8, pp. 2\u201314. EasyChair (2012)"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) Theory and Applications of Satisfiability Testing - SAT 2009. pp. 244\u2013257. Springer, Berlin, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02777-2_24"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Tseitin, G.C.: On the complexity of derivations in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Mathematics and Mathematical Logic, Part II, pp. 115\u2013125 (1968)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"issue":"1","key":"1_CR21","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. Journal of the ACM 34(1), 209\u2013219 (1987)","journal-title":"Journal of the ACM"},{"issue":"3","key":"1_CR22","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/S0167-6377(98)00052-2","volume":"23","author":"JP Warners","year":"1998","unstructured":"Warners, J.P., van Maaren, H.: A two-phase algorithm for solving a class of hard satisfiability problems. Operations Research Letters 23(3), 81\u201388 (1998). ISSN 0167-6377","journal-title":"Operations Research Letters"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2020"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-51825-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T11:40:36Z","timestamp":1667216436000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-51825-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030518240","9783030518257"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-51825-7_1","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":"26 June 2020","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":"Alghero","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"3 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sat2020.idea-researchlab.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":"69","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":"25","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":"9","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":"36% - 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","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":"6","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"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"}]}}