{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T02:49:21Z","timestamp":1782874161854,"version":"3.54.5"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227515","type":"print"},{"value":"9783032227522","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T00:00:00Z","timestamp":1776297600000},"content-version":"vor","delay-in-days":105,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22752-2_5","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T21:52:35Z","timestamp":1776289955000},"page":"89-109","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Orbitopal Fixing in SAT"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-5992-8433","authenticated-orcid":false,"given":"Markus","family":"Anders","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3588-4873","authenticated-orcid":false,"given":"Cayden","family":"Codel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,16]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Aloul, F.A., Markov, I.L., Sakallah, K.A.: Shatter: efficient symmetry-breaking for boolean satisfiability. In: Proceedings of the 40th Design Automation Conference, DAC 2003, Anaheim, CA, USA, June 2-6, 2003. pp. 836\u2013839. ACM (2003). https:\/\/doi.org\/10.1145\/775832.776042","DOI":"10.1145\/775832.776042"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult instances of boolean satisfiability in the presence of symmetry. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 22(9), 1117\u20131137 (2003). https:\/\/doi.org\/10.1109\/TCAD.2003.816218","DOI":"10.1109\/TCAD.2003.816218"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Anders, M., Brenner, S., Rattan, G.: Satsuma: Structure-based symmetry breaking in SAT. In: 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, August 21-24, 2024, Pune, India. LIPIcs, vol.\u00a0305, pp. 4:1\u20134:23. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2024.4","DOI":"10.4230\/LIPICS.SAT.2024.4"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Anders, M., Schweitzer, P.: Parallel computation of combinatorial symmetries. In: 29th Annual European Symposium on Algorithms, ESA 2021, September 6-8, 2021, Lisbon, Portugal (Virtual Conference). LIPIcs, vol.\u00a0204, pp. 6:1\u20136:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.ESA.2021.6","DOI":"10.4230\/LIPICS.ESA.2021.6"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Anders, M., Schweitzer, P.: Search problems in trees with symmetries: Near optimal traversal strategies for individualization-refinement algorithms. In: 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference). LIPIcs, vol.\u00a0198, pp. 16:1\u201316:21. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.ICALP.2021.16","DOI":"10.4230\/LIPICS.ICALP.2021.16"},{"key":"5_CR6","unstructured":"Balyo, T., Heule, M.J.H., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.): Proceedings of SAT Competition 2022: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, Helsinki Institute for Information Technology (2022)"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Bendotti, P., Fouilhoux, P., Rottner, C.: Orbitopal fixing for the full (sub-)orbitope and application to the unit commitment problem. Mathematical Programming 186(1), 337\u2013372 (2021). https:\/\/doi.org\/10.1007\/s10107-019-01457-1","DOI":"10.1007\/s10107-019-01457-1"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL 2.0. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 133\u2013152. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_7","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA336","DOI":"10.3233\/FAIA336"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Bogaerts, B., Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: Certified dominance and symmetry breaking for combinatorial optimisation. J. Artif. Intell. Res. 77, 1539\u20131589 (2023). https:\/\/doi.org\/10.1613\/JAIR.1.14296","DOI":"10.1613\/JAIR.1.14296"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Brown, S.T., Buitrago, P., Hanna, E., Sanielevici, S., Scibek, R., Nystrom, N.A.: Bridges-2: A platform for rapidly-evolving and data intensive research. In: Practice and Experience in Advanced Research Computing 2021: Evolution Across All Dimensions. PEARC \u201921, Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3437359.3465593","DOI":"10.1145\/3437359.3465593"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Buss, S., Thapen, N.: DRAT and propagation redundancy proofs without new variables. Logical Methods in Computer Science Volume 17, Issue 2 (Apr 2021). https:\/\/doi.org\/10.23638\/LMCS-17(2:12)2021","DOI":"10.23638\/LMCS-17(2:12)2021"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Codel, C.R., Avigad, J., Heule, M.J.H.: Verified substitution redundancy checking. In: Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024. pp. 186\u2013196. IEEE (2024). https:\/\/doi.org\/10.34727\/2024\/ISBN.978-3-85448-065-5_24","DOI":"10.34727\/2024\/ISBN.978-3-85448-065-5_24"},{"key":"5_CR14","unstructured":"Crawford, J.M., Ginsberg, M.L., Luks, E.M., Roy, A.: Symmetry-breaking predicates for search problems. In: Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR\u201996), Cambridge, Massachusetts, USA, November 5-8, 1996. pp. 148\u2013159. Morgan Kaufmann (1996)"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Devriendt, J., Bogaerts, B., Bruynooghe, M.: Symmetric explanation learning: Effective dynamic symmetry handling for SAT. In: Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10491, pp. 83\u2013100. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_6","DOI":"10.1007\/978-3-319-66263-3_6"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Improved static symmetry breaking for SAT. In: Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09710, pp. 104\u2013122. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_8","DOI":"10.1007\/978-3-319-40970-2_8"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Devriendt, J., Bogaerts, B., Cat, B.D., 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, November 7-9, 2012. pp. 49\u201356. IEEE Computer Society (2012). https:\/\/doi.org\/10.1109\/ICTAI.2012.16","DOI":"10.1109\/ICTAI.2012.16"},{"key":"5_CR18","doi-asserted-by":"publisher","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: Principles and Practice of Constraint Programming - CP 2002, 8th International Conference, CP 2002, Ithaca, NY, USA, September 9-13, 2002, Proceedings. Lecture Notes in Computer Science, vol.\u00a02470, pp. 462\u2013476. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-46135-3_31","DOI":"10.1007\/3-540-46135-3_31"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Gent, I.P., Petrie, K.E., Puget, J.: Symmetry in constraint programming. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, Foundations of Artificial Intelligence, vol.\u00a02, pp. 329\u2013376. Elsevier (2006). https:\/\/doi.org\/10.1016\/S1574-6526(06)80014-3","DOI":"10.1016\/S1574-6526(06)80014-3"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Gocht, S., Nordstr\u00f6m, J.: Certifying parity reasoning efficiently using pseudo-boolean proofs. In: Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021. pp. 3768\u20133777. AAAI Press (2021). https:\/\/doi.org\/10.1609\/AAAI.V35I5.16494","DOI":"10.1609\/AAAI.V35I5.16494"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Strong extension-free proof systems. Journal of Automated Reasoning 64(3), 533\u2013554 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09516-0","DOI":"10.1007\/s10817-019-09516-0"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Hojny, C., Pfetsch, M.E.: Polytopes associated with symmetry handling. Math. Program. 175(1-2), 197\u2013240 (2019). https:\/\/doi.org\/10.1007\/S10107-018-1239-7","DOI":"10.1007\/S10107-018-1239-7"},{"key":"5_CR23","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Automated Reasoning. pp. 355\u2013370 (2012)"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Junttila, T.A., Karppa, M., Kaski, P., Kohonen, J.: An adaptive prefix-assignment technique for symmetry reduction. J. Symb. Comput. 99, 21\u201349 (2020). https:\/\/doi.org\/10.1016\/J.JSC.2019.03.002","DOI":"10.1016\/J.JSC.2019.03.002"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Junttila, T.A., Kaski, P.: Engineering an efficient canonical labeling tool for large and sparse graphs. In: Proceedings of the Nine Workshop on Algorithm Engineering and Experiments, ALENEX 2007, New Orleans, Louisiana, USA, January 6, 2007. SIAM (2007). https:\/\/doi.org\/10.1137\/1.9781611972870.13","DOI":"10.1137\/1.9781611972870.13"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Junttila, T.A., Kaski, P.: Conflict propagation and component recursion for canonical labeling. In: Theory and Practice of Algorithms in (Computer) Systems - First International ICST Conference, TAPAS 2011, Rome, Italy, April 18-20, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06595, pp. 151\u2013162. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-19754-3_16","DOI":"10.1007\/978-3-642-19754-3_16"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Kaibel, V., Peinhardt, M., Pfetsch, M.E.: Orbitopal fixing. Discrete Optimization 8(4), 595\u2013610 (2011). https:\/\/doi.org\/10.1016\/j.disopt.2011.07.001","DOI":"10.1016\/j.disopt.2011.07.001"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Luks, E.M.: Permutation groups and polynomial-time computation. In: Groups And Computation, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, October 7-10, 1991. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a011, pp. 139\u2013175. DIMACS\/AMS (1991). https:\/\/doi.org\/10.1090\/DIMACS\/011\/11","DOI":"10.1090\/DIMACS\/011\/11"},{"key":"5_CR29","doi-asserted-by":"publisher","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119\u2013161 (2011). https:\/\/doi.org\/10.1016\/J.COSREV.2010.09.009","DOI":"10.1016\/J.COSREV.2010.09.009"},{"key":"5_CR30","unstructured":"McKay, B.D.: Practical graph isomorphism. In: 10th. Manitoba Conference on Numerical Mathematics and Computing (Winnipeg, 1980). pp. 45\u201387 (1981)"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"McKay, B.D., Piperno, A.: Practical graph isomorphism, II. J. Symb. Comput. 60, 94\u2013112 (2014). https:\/\/doi.org\/10.1016\/J.JSC.2013.09.003","DOI":"10.1016\/J.JSC.2013.09.003"},{"key":"5_CR32","unstructured":"Mexi, G., Kamp, D., Shinano, Y., Pu, S., Hoen, A., Bestuzheva, K., Hojny, C., Walter, M., Pfetsch, M.E., Pokutta, S., Koch, T.: State-of-the-art methods for pseudo-boolean solving with SCIP (2025), https:\/\/arxiv.org\/abs\/2501.03390"},{"key":"5_CR33","doi-asserted-by":"publisher","unstructured":"Pfetsch, M.E., Rehn, T.: A computational comparison of symmetry handling methods for mixed integer programs. Math. Program. Comput. 11(1), 37\u201393 (2019). https:\/\/doi.org\/10.1007\/S12532-018-0140-Y","DOI":"10.1007\/S12532-018-0140-Y"},{"key":"5_CR34","unstructured":"Piperno, A.: Search space contraction in canonical labeling of graphs (preliminary version). CoRR abs\/0804.4881 (2008), http:\/\/arxiv.org\/abs\/0804.4881"},{"key":"5_CR35","doi-asserted-by":"publisher","unstructured":"Rebola-Pardo, A.: Even shorter proofs without new variables. In: Mahajan, M., Slivovsky, F. (eds.) 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0271, pp. 22:1\u201322:20. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2023). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2023.22","DOI":"10.4230\/LIPIcs.SAT.2023.22"},{"key":"5_CR36","doi-asserted-by":"publisher","unstructured":"Sabharwal, A.: SymChaff: exploiting symmetry in a structure-aware satisfiability solver. Constraints An Int. J. 14(4), 478\u2013505 (2009). https:\/\/doi.org\/10.1007\/S10601-008-9060-1","DOI":"10.1007\/S10601-008-9060-1"},{"key":"5_CR37","doi-asserted-by":"publisher","unstructured":"Seress, \u00c1.: Permutation Group Algorithms. Cambridge Tracts in Mathematics, Cambridge University Press (2003). https:\/\/doi.org\/10.1017\/CBO9780511546549","DOI":"10.1017\/CBO9780511546549"},{"key":"5_CR38","doi-asserted-by":"publisher","unstructured":"Sheng, A., Reeves, J.E., Heule, M.J.H.: Reencoding unique literal clauses. In: 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, August 12-15, 2025, Glasgow, Scotland. LIPIcs, vol.\u00a0341, pp. 29:1\u201329:21. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2025). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2025.29","DOI":"10.4230\/LIPICS.SAT.2025.29"},{"key":"5_CR39","doi-asserted-by":"publisher","unstructured":"Sims, C.C.: Computational methods in the study of permutation groups. In: Computational Problems in Abstract Algebra, pp. 169\u2013183. Pergamon (1970). https:\/\/doi.org\/10.1016\/B978-0-08-012975-4.50020-5","DOI":"10.1016\/B978-0-08-012975-4.50020-5"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22752-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T02:39:01Z","timestamp":1782873541000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22752-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227515","9783032227522"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22752-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"16 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","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":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}