{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:56Z","timestamp":1776333536687,"version":"3.51.2"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319662626","type":"print"},{"value":"9783319662633","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66263-3_6","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T04:05:11Z","timestamp":1502165111000},"page":"83-100","source":"Crossref","is-referenced-by-count":12,"title":["Symmetric Explanation Learning: Effective Dynamic Symmetry Handling for SAT"],"prefix":"10.1007","author":[{"given":"Jo","family":"Devriendt","sequence":"first","affiliation":[]},{"given":"Bart","family":"Bogaerts","sequence":"additional","affiliation":[]},{"given":"Maurice","family":"Bruynooghe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"key":"6_CR1","unstructured":"Aloul, F., Ramani, A., Markov, I., Sakallah, K.: Solving difficult SAT instances in the presence of symmetry. In: 39th Design Automation Conference, 2002 Proceedings, pp. 731\u2013736 (2002)"},{"issue":"1","key":"6_CR2","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/s10472-010-9173-2","volume":"57","author":"FA Aloul","year":"2009","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Dynamic symmetry-breaking for boolean satisfiability. Ann. Math. Artif. Intell. 57(1), 59\u201373 (2009)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"5","key":"6_CR3","doi-asserted-by":"crossref","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":"6_CR4","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) IJCAI, pp. 399\u2013404 (2009)"},{"key":"6_CR5","unstructured":"Benhamou, B., Nabhani, T., Ostrowski, R., Sa\u00efdi, M.R.: Dynamic symmetry breaking in the satisfiability problem. In: Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-16, Dakar, Senegal, 25 April \u20131 May 2010"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Benhamou, B., Nabhani, T., Ostrowski, R., Sa\u00efdi, M.R.: Enhancing clause learning by symmetry in SAT solvers. In: Proceedings of the 2010 22nd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2010, vol. 01, pp. 329\u2013335 (2010). http:\/\/dx.doi.org\/10.1109\/ICTAI.2010.55","DOI":"10.1109\/ICTAI.2010.55"},{"issue":"1","key":"6_CR7","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/BF00881844","volume":"12","author":"B Benhamou","year":"1994","unstructured":"Benhamou, B., Sa\u00efs, L.: Tractability through symmetries in propositional calculus. J. Autom. Reason. 12(1), 89\u2013102 (1994). http:\/\/dx.doi.org\/10.1007\/BF00881844","journal-title":"J. Autom. Reason."},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-34188-5_1","volume-title":"Hardware and Software: Verification and Testing","author":"A Biere","year":"2012","unstructured":"Biere, A.: Preprocessing and inprocessing techniques in SAT. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, p. 1. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-34188-5_1"},{"key":"6_CR9","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1613\/jair.601","volume":"10","author":"E Birnbaum","year":"1999","unstructured":"Birnbaum, E., Lozinskii, E.L.: The good old Davis-Putnam procedure helps counting models. J. Artif. Intell. Res. 10, 457\u2013477 (1999)","journal-title":"J. Artif. Intell. Res."},{"key":"6_CR10","unstructured":"Crawford, J.M., Ginsberg, M.L., Luks, E.M., Roy, A.: Symmetry-breaking predicates for search problems. In: Principles of Knowledge Representation and Reasoning, pp. 148\u2013159. Morgan Kaufmann (1996)"},{"key":"6_CR11","unstructured":"Devriendt, J.: Binaries, experimental results and benchmark instances for \u201csymmetric explanation learning: effective dynamic symmetry handling for SAT\u201d. bitbucket.org\/krr\/sat_symmetry_experiments"},{"key":"6_CR12","unstructured":"Devriendt, J.: An implementation of symmetric explanation learning in Glucose on Bitbucket. bitbucket.org\/krr\/glucose-sel"},{"key":"6_CR13","unstructured":"Devriendt, J.: An implementation of symmetry propagation in MiniSat on Github. github.com\/JoD\/minisat-SPFS"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-319-40970-2_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"J Devriendt","year":"2016","unstructured":"Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Improved static symmetry breaking for SAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 104\u2013122. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_8"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Devriendt, J., Bogaerts, B., De Cat, B., Denecker, M., Mears, C.: Symmetry propagation: improved dynamic symmetry breaking in SAT. In: IEEE 24th International Conference on Tools with Artificial Intelligence, ICTAI 2012, Athens, Greece, pp. 49\u201356. IEEE Computer Society, 7\u20139 November 2012. http:\/\/dx.doi.org\/10.1109\/ICTAI.2012.16","DOI":"10.1109\/ICTAI.2012.16"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61\u201375. Springer, Heidelberg (2005). doi: 10.1007\/11499107_5"},{"key":"6_CR17","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). doi: 10.1007\/978-3-540-24605-3_37"},{"key":"6_CR18","unstructured":"Gent, I.P., Smith, B.M.: Symmetry breaking in constraint programming. In: Proceedings of ECAI-2000, pp. 599\u2013603. IOS Press (2000)"},{"key":"6_CR19","doi-asserted-by":"crossref","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, 297\u2013308 (1985). Third Conference on Foundations of Software Technology and Theoretical Computer Science. http:\/\/www.sciencedirect.com\/science\/article\/pii\/0304397585901446","journal-title":"Theor. Comput. Sci."},{"key":"6_CR20","unstructured":"Heule, M., Keur, A., Maaren, H.V., Stevens, C., Voortman, M.: CNF symmetry breaking options in conflict driven SAT solving (2005)"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Junttila, T., Kaski, P.: Engineering an efficient canonical labeling tool for large and sparse graphs. In: Applegate, D., Brodal, G.S., Panario, D., Sedgewick, R. (eds.) Proceedings of the Ninth Workshop on Algorithm Engineering and Experiments and the Fourth Workshop on Analytic Algorithms and Combinatorics, pp. 135\u2013149. SIAM (2007)","DOI":"10.1137\/1.9781611972870.13"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-642-14186-7_11","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"H Katebi","year":"2010","unstructured":"Katebi, H., Sakallah, K.A., Markov, I.L.: Symmetry and satisfiability: an update. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 113\u2013127. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14186-7_11"},{"issue":"3","key":"6_CR23","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/BF00265682","volume":"22","author":"B Krishnamurthy","year":"1985","unstructured":"Krishnamurthy, B.: Short proofs for tricky formulas. Acta Inf. 22(3), 253\u2013275 (1985). http:\/\/dl.acm.org\/citation.cfm?id=4336.4338","journal-title":"Acta Inf."},{"issue":"5","key":"6_CR24","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"6_CR25","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1016\/j.jsc.2013.09.003","volume":"60","author":"BD McKay","year":"2014","unstructured":"McKay, B.D., Piperno, A.: Practical graph isomorphism, II. J. Symbolic Comput. 60, 94\u2013112 (2014). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0747717113001193","journal-title":"J. Symbolic Comput."},{"issue":"3","key":"6_CR26","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/s10601-013-9154-2","volume":"19","author":"C Mears","year":"2014","unstructured":"Mears, C., Garc\u00eda de la Banda, M., Demoen, B., Wallace, M.: Lightweight dynamic symmetry breaking. Constraints 19(3), 195\u2013242 (2014). http:\/\/dx.doi.org\/10.1007\/s10601-013-9154-2","journal-title":"Constraints"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC 2001, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"6_CR28","doi-asserted-by":"crossref","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. Artif. Intell. 175(2), 512\u2013525 (2011). http:\/\/dx.doi.org\/10.1016\/j.artint.2010.10.002","journal-title":"Artif. Intell."},{"issue":"4","key":"6_CR29","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1007\/s10601-008-9060-1","volume":"14","author":"A Sabharwal","year":"2009","unstructured":"Sabharwal, A.: SymChaff: exploiting symmetry in a structure-aware satisfiability solver. Constraints 14(4), 478\u2013505 (2009). http:\/\/dx.doi.org\/10.1007\/s10601-008-9060-1","journal-title":"Constraints"},{"key":"6_CR30","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., van Heule, M.J.H., Maaren, H.: Dynamic symmetry breaking by simulating zykov contraction. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 223\u2013236. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02777-2_22"},{"key":"6_CR31","unstructured":"S\u00f6rensson, N., E\u00e9n, N.: MiniSat v1.13 - a Sat solver with conflict-clause minimization. 2005. sat-2005 poster. Technical report (2005)"},{"key":"6_CR32","unstructured":"Trick, M.: Network resources for coloring a graph (1994). mat.gsia.cmu.edu\/COLOR\/color.html"},{"key":"6_CR33","unstructured":"Walsh, T.: Symmetry breaking constraints: Recent results. CoRR abs\/1204.3348 (2012)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66263-3_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T23:35:45Z","timestamp":1569972945000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}