{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T18:09:50Z","timestamp":1776881390594,"version":"3.51.2"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319214009","type":"print"},{"value":"9783319214016","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","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":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_40","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"591-606","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Expressing Symmetry Breaking in DRAT Proofs"],"prefix":"10.1007","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[]},{"suffix":"Jr.","given":"Warren A.","family":"Hunt","sequence":"additional","affiliation":[]},{"given":"Nathan","family":"Wetzler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"40_CR1","unstructured":"Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: KR 1996, pp. 148\u2013159. Morgan Kaufmann (1996)"},{"key":"40_CR2","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult sat instances in the presence of symmetry. In: Proceedings of the 39th Design Automation Conference, pp. 731\u2013736 (2002)","DOI":"10.1145\/513918.514102"},{"key":"40_CR3","unstructured":"Gent, I.P., Smith, B.M.: Symmetry breaking in constraint programming. In: Horn, W. (ed.) ECAI 2000, pp. 599\u2013603. IOS Press (2000)"},{"key":"40_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt Jr, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Heidelberg (2014)"},{"key":"40_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/978-3-319-09284-3_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"B Konev","year":"2014","unstructured":"Konev, B., Lisitsa, A.: A SAT attack on the Erd\u0151s discrepancy conjecture. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 219\u2013226. Springer, Heidelberg (2014)"},{"issue":"1","key":"40_CR6","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1080\/10586458.2008.10129025","volume":"17","author":"M Kouril","year":"2008","unstructured":"Kouril, M., Paul, J.L.: The van der Waerden number W(2, 6) is 1132. Exp. Math. 17(1), 53\u201361 (2008)","journal-title":"Exp. Math."},{"key":"40_CR7","doi-asserted-by":"crossref","unstructured":"Codish, M., Cruz-Filipe, L., Frank, M., Schneider-Kamp, P.: Twenty-five comparators is optimal when sorting nine inputs (and twenty-nine for ten). In: ICTAI 2014, pp. 186\u2013193. IEEE Computer Society (2014)","DOI":"10.1109\/ICTAI.2014.36"},{"issue":"5","key":"40_CR8","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1109\/TC.2006.75","volume":"55","author":"FA Aloul","year":"2006","unstructured":"Aloul, F.A., Sakallah, K.A., Markov, I.L.: Efficient symmetry breaking for boolean satisfiability. IEEE Trans. Comput. 55(5), 549\u2013558 (2006)","journal-title":"IEEE Trans. Comput."},{"key":"40_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-642-02777-2_22","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"B Schaafsma","year":"2009","unstructured":"Schaafsma, B., Heule, M.J.H., van Maaren, H.: Dynamic symmetry breaking by simulating zykov contraction. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 223\u2013236. Springer, Heidelberg (2009)"},{"key":"40_CR10","unstructured":"Radziszowski, S.P.: Small Ramsey numbers. Electron. J. Comb. #DS1 (2014)"},{"key":"40_CR11","unstructured":"Wetzler, N.D.: Efficient, mechanically-verified validation of satisfiability solvers. Ph.D. dissertation, The University of Texas at Austin, May 2015"},{"key":"40_CR12","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96\u201397","author":"O Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Appl. Math. 96\u201397, 149\u2013176 (1999)","journal-title":"Discrete Appl. Math."},{"key":"40_CR13","unstructured":"Zhang, L., Malik, S.: Validating sat solvers using an independent resolution-based checker: practical implementations and other applications. In: DATE, pp. 10880\u201310885 (2003)"},{"key":"40_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"issue":"2\u20134","key":"40_CR15","first-page":"75","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A.: Picosat essentials. JSAT 4(2\u20134), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"40_CR16","doi-asserted-by":"crossref","unstructured":"Van Gelder, A.: Verifying rup proofs of propositional unsatisfiability. In: ISAIM (2008)","DOI":"10.1007\/978-3-540-72788-0_31"},{"key":"40_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-38574-2_24","volume-title":"Automated Deduction \u2013 CADE-24","author":"MJH Heule","year":"2013","unstructured":"Heule, M.J.H., Hunt Jr, W.A., Wetzler, N.: Verifying refutations with extended resolution. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 345\u2013359. Springer, Heidelberg (2013)"},{"key":"40_CR18","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.: Trimming while checking clausal proofs. In: Formal Methods in Computer-Aided Design, pp. 181\u2013188. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"issue":"8","key":"40_CR19","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1002\/stvr.1549","volume":"24","author":"MJH Heule","year":"2014","unstructured":"Heule, M.J.H., Hunt Jr, W.A., Wetzler, N.: Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test. Verif. Reliab. (STVR) 24(8), 593\u2013607 (2014)","journal-title":"Softw. Test. Verif. Reliab. (STVR)"},{"key":"40_CR20","series-title":"Lecture Notes in Computer Science","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, vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"40_CR21","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)"},{"key":"40_CR22","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1142\/S0129626492000337","volume":"2","author":"I Parberry","year":"1992","unstructured":"Parberry, I.: The pairwise sorting network. Parallel Process. Lett. 2, 205\u2013211 (1992)","journal-title":"Parallel Process. Lett."},{"key":"40_CR23","doi-asserted-by":"crossref","unstructured":"Batcher, K.E.: Sorting networks and their applications. In: Proceedings of Spring Joint Computer Conference, AFIPS 1968, pp. 307\u2013314. ACM (1968)","DOI":"10.1145\/1468075.1468121"},{"key":"40_CR24","doi-asserted-by":"crossref","unstructured":"Darga, P.T., Liffiton, M.H., Sakallah, K.A., Markov, I.L.: Exploiting structure in symmetry detection for cnf. In: DAC 2004, pp. 530\u2013534. ACM (2004)","DOI":"10.1145\/996566.996712"},{"key":"40_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-39634-2_18","volume-title":"Interactive Theorem Proving","author":"N Wetzler","year":"2013","unstructured":"Wetzler, N., Heule, M.J.H., Hunt Jr, W.A.: Mechanical verification of SAT refutations with extended resolution. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 229\u2013244. Springer, Heidelberg (2013)"},{"key":"40_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-14186-7_6","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"R Brummayer","year":"2010","unstructured":"Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 44\u201357. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T13:27:00Z","timestamp":1676467620000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}