{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:02:27Z","timestamp":1750309347705,"version":"3.41.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2024,7,31]],"date-time":"2024-07-31T00:00:00Z","timestamp":1722384000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2024,7,31]]},"abstract":"<jats:p>\n            We propose a novel SAT-based approach to graph generation. Our approach utilizes the interaction between a CDCL SAT solver and a special symmetry propagator where the SAT solver runs on an encoding of the desired graph property. The symmetry propagator checks partially generated graphs for minimality with respect to a lexicographic ordering during the solving process. This approach has several advantages over a static symmetry breaking: (i) symmetries are detected early in the generation process, (ii) symmetry breaking is seamlessly integrated into the CDCL procedure, and (iii) the propagator performs a complete symmetry breaking without causing a prohibitively large initial encoding. We instantiate our approach by generating extremal graphs with certain restrictions in terms of forbidden subgraphs and diameter. In particular, we could confirm the Murty\u2013Simon Conjecture (1979) on diameter-2-critical graphs for graphs up to 19 vertices and prove the exact number of Ramsey graphs\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathcal{R}(3,5,n)\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            and\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathcal{R}(4,4,n)\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            .\n          <\/jats:p>","DOI":"10.1145\/3670405","type":"journal-article","created":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T04:21:22Z","timestamp":1717993282000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["SAT Modulo Symmetries for Graph Generation and Enumeration"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1838-8344","authenticated-orcid":false,"given":"Markus","family":"Kirchweger","sequence":"first","affiliation":[{"name":"Algorithms and Complexity Group, TU Wien, Vienna, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8994-1656","authenticated-orcid":false,"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[{"name":"Algorithms and Complexity Group, TU Wien, Vienna, Austria"}]}],"member":"320","published-online":{"date-parts":[[2024,7,31]]},"reference":[{"key":"e_1_3_2_2_1","unstructured":"2023a. The On-Line Encyclopedia of Integer Sequences. Number of Connected Graphs with n Nodes. Retrieved from http:\/\/oeis.org\/A001349"},{"key":"e_1_3_2_3_1","unstructured":"2023b. The On-Line Encyclopedia of Integer Sequences. Number of Connected Labeled Graphs with n Nodes. Retrieved from http:\/\/oeis.org\/A001187"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2014.11.021"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808746"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020533821509"},{"key":"e_1_3_2_7_1","volume-title":"Extremal Graph Theory","author":"Bollob\u00e1s B\u00e9la","year":"1978","unstructured":"B\u00e9la Bollob\u00e1s. 1978. Extremal Graph Theory. Academic Press."},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(79)90129-8"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1002\/jgt.20111"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-014-9163-9"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-44953-1_11"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-018-9294-5"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.disc.2019.06.023"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_6"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_8"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2012.16"},{"key":"e_1_3_2_18_1","first-page":"623","article-title":"On a problem in the theory of graphs","volume":"7","author":"Erd\u0151s P.","year":"1962","unstructured":"P. Erd\u0151s and A. R\u00e9nyi. 1962. On a problem in the theory of graphs. Publ. Math. Inst. Hung. Acad. Sci. 7A, 623\u2013641.","journal-title":"Publ. Math. Inst. Hung. Acad. Sci."},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45578-7_7"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(87)90174-9"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.SAT.2023.8"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1002\/jgt.3190170511"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.ICLP.2016.2"},{"key":"e_1_3_2_24_1","unstructured":"Martin Gebser Roland Kaminski Benjamin Kaufmann and Torsten Schaub. 2014. Clingo = ASP + Control: Preliminary Report. http:\/\/arXiv.org\/abs\/1405.3694arXiv:1405.3694."},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1574-6526(06)80014-3"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.2478\/s11533-014-0449-3"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10878-013-9651-7"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/S11786-019-00397-5"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10601-016-9244-Z"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i02.5513"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-33271-5_10"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2023\/216"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SAT.2023.13"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SAT.2022.4"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SAT.2023.14"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5170575"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CP.2021.34"},{"key":"e_1_3_2_38_1","unstructured":"Markus Kirchweger and Stefan Szeider. 2024. Computing Small Rainbow Cycle Numbers with SAT Modulo Symmetries. To appear."},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2306.13319"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jctb.2015.11.004"},{"key":"e_1_3_2_41_1","first-page":"60","article-title":"Problem 28","volume":"10","author":"Mantel W.","year":"1907","unstructured":"W. Mantel. 1907. Problem 28. Wiskundige Opgaven 10, 60\u201361.","journal-title":"Wiskundige Opgaven"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_9"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2013.09.003"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1002\/jgt.3190190304"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_6"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068412000130"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45193-8_40"},{"issue":"1","key":"e_1_3_2_48_1","first-page":"1","article-title":"The List of Diameter-2-Critical Graphs with at Most 10 Nodes","volume":"16","author":"Radosavljevi\u0107 Jovan","year":"2020","unstructured":"Jovan Radosavljevi\u0107 and Miodrag \u017divkovi\u0107. 2020. The List of Diameter-2-Critical Graphs with at Most 10 Nodes. IPSI Trans. Adv. Res. 16, 1 (Jan. 2020), 1\u20135. Retrieved from http:\/\/ipsitransactions.org\/journals\/papers\/tar\/2020jan\/p9.pdf.","journal-title":"IPSI Trans. Adv. Res."},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.37236\/21"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_22"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2007.10.029"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0012-365X(00)00265-XCombinatorics"},{"key":"e_1_3_2_54_1","volume-title":"Combinatorial Mathematics","author":"West Douglas B.","year":"2021","unstructured":"Douglas B. West. 2021. Combinatorial Mathematics. Cambridge University Press. 220 pages."},{"key":"e_1_3_2_55_1","volume-title":"Proceedings of the 27th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201924)","author":"Zhang Tianwei","year":"2024","unstructured":"Tianwei Zhang, Tom\u00e1\u0161 Peitl, and Stefan Szeider. 2024. Small Unsatisfiable \\(k\\) -CNFs with Bounded Literal Occurrence. In Proceedings of the 27th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201924), LIPIcs. Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CP.2023.39"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3670405","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3670405","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:05:38Z","timestamp":1750291538000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3670405"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,31]]},"references-count":55,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,7,31]]}},"alternative-id":["10.1145\/3670405"],"URL":"https:\/\/doi.org\/10.1145\/3670405","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2024,7,31]]},"assertion":[{"value":"2023-11-08","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-05-05","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-07-31","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}