{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:51:45Z","timestamp":1764402705554,"version":"3.37.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319409696"},{"type":"electronic","value":"9783319409702"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40970-2_8","type":"book-chapter","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T07:14:55Z","timestamp":1465542895000},"page":"104-122","source":"Crossref","is-referenced-by-count":32,"title":["Improved Static Symmetry Breaking 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":[]},{"given":"Marc","family":"Denecker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F., Ramani, A., Markov, I., Sakallah, K.: Solving difficult SAT instances in the presence of symmetry. In: Proceedings of the 39th Design Automation Conference, 2002, pp. 731\u2013736 (2002)","DOI":"10.1109\/DAC.2002.1012719"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Markov, I.L., Sakallah, K.A.: Shatter: efficient symmetry-breaking for boolean satisfiability. In: Design Automation Conference, pp. 836\u2013839 (2003)","DOI":"10.1145\/775832.776042"},{"issue":"5","key":"8_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":"8_CR4","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) IJCAI, pp. 399\u2013404 (2009)"},{"key":"8_CR5","unstructured":"Balint, A., Belov, A., Heule, M.J., J\u00e4rvisalo, M.: The 2013 international SAT competition (2013). satcompetition.org\/2013"},{"key":"8_CR6","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":"8_CR7","unstructured":"Devriendt, J., Bogaerts, B.: BreakID, a symmetry breaking preprocessor for SAT solvers (2015). bitbucket.org\/krr\/breakid"},{"key":"8_CR8","unstructured":"Devriendt, J., Bogaerts, B., Bruynooghe, M.: BreakIDGlucose: On the importance of row symmetry. In: Proceedings of the Fourth International Workshop on the Cross-Fertilization Between CSP and SAT (CSPSAT) (2014). http:\/\/lirias.kuleuven.be\/handle\/123456789\/456639"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"462","DOI":"10.1007\/3-540-46135-3_31","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"P Flener","year":"2002","unstructured":"Flener, P., Frisch, A.M., Hnich, B., Kiziltan, Z., Miguel, I., Pearson, J., Walsh, T.: Breaking row and column symmetries in matrix models. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 462\u2013477. Springer, Heidelberg (2002). http:\/\/dx.doi.org\/10.1007\/3-540-46135-3_31"},{"key":"8_CR11","unstructured":"The GAP Group: GAP - Groups, Algorithms, and Programming, Version 4.7.9 (2015). www.gap-system.org"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297\u2013308 (1985). http:\/\/www.sciencedirect.com\/science\/article\/pii\/0304397585901446 . Third Conference on Foundations of Software Technology and Theoretical Computer Science","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"729","DOI":"10.1007\/978-3-642-23786-7_55","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"C Jefferson","year":"2011","unstructured":"Jefferson, C., Petrie, K.E.: Automatic generation of constraints for partial symmetry breaking. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 729\u2013743. Springer, Heidelberg (2011). http:\/\/dx.doi.org\/10.1007\/978-3-642-23786-7_55"},{"key":"8_CR14","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":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","first-page":"422","volume-title":"Principles and Practice of Constraint Programming","author":"JHM Lee","year":"2012","unstructured":"Lee, J.H.M., Li, J.: Increasing symmetry breaking by preserving target symmetries. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 422\u2013438. Springer, Heidelberg (2012). http:\/\/dx.doi.org\/10.1007\/978-3-642-33558-7_32"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/978-3-540-72788-0_6","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"I Lynce","year":"2007","unstructured":"Lynce, I., Marques-Silva, J.: Breaking symmetries in SAT matrix models. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 22\u201327. Springer, Heidelberg (2007). http:\/\/dx.doi.org\/10.1007\/978-3-540-72788-0_6"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1007\/3-540-46135-3_29","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"I McDonald","year":"2002","unstructured":"McDonald, I., Smith, B.: Partial symmetry breaking. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 431\u2013445. Springer, Heidelberg (2002). http:\/\/dx.doi.org\/10.1007\/3-540-46135-3_29"},{"key":"8_CR19","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. J. Symbolic Comput. 60, 94\u2013112 (2014). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0747717113001193","journal-title":"J. Symbolic Comput."},{"key":"8_CR20","unstructured":"Puget, J.F.: Breaking symmetries in all-different problems. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence, IJCAI 2005, pp. 272\u2013277 (2005)"},{"issue":"4","key":"8_CR21","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":"8_CR22","first-page":"289","volume-title":"Handbook of Satisfiability","author":"KA Sakallah","year":"2009","unstructured":"Sakallah, K.A.: Symmetry and satisfiability. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 185, pp. 289\u2013338. IOS Press, Amsterdam (2009)"},{"key":"8_CR23","doi-asserted-by":"crossref","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). http:\/\/dx.doi.org\/10.1007\/978-3-642-02777-2_22","DOI":"10.1007\/978-3-642-02777-2_22"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Seress, \u00c1.: Permutation Group Algorithms. Cambridge University Press (2003). cambridgeBooksOnline. http:\/\/dx.doi.org\/10.1017\/CBO9780511546549","DOI":"10.1017\/CBO9780511546549"},{"issue":"12","key":"8_CR25","doi-asserted-by":"crossref","first-page":"1539","DOI":"10.1016\/j.dam.2005.10.018","volume":"155","author":"I Shlyakhter","year":"2007","unstructured":"Shlyakhter, I.: Generating effective symmetry-breaking predicates for search problems. Discrete Appl. Math. 155(12), 1539\u20131548 (2007). http:\/\/dx.doi.org\/10.1016\/j.dam.2005.10.018","journal-title":"Discrete Appl. Math."},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Urquhart, A.: Hard examples for resolution. J. ACM 34(1), 209\u2013219. http:\/\/doi.acm.org\/10.1145\/7531.8928","DOI":"10.1145\/7531.8928"},{"key":"8_CR27","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 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40970-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T10:08:42Z","timestamp":1568023722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40970-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409696","9783319409702"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40970-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}