{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T07:14:22Z","timestamp":1761549262107,"version":"build-2065373602"},"reference-count":17,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2023,1,4]],"date-time":"2023-01-04T00:00:00Z","timestamp":1672790400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SAT"],"abstract":"<jats:p>We define a distance function on propositional formulas in CNF as a measure of non-isomorphism of formulas: the larger the distance between two formulas is, the further they are from being isomorphic. This distance induces a metric on isomorphism classes of formulas. We show how this distance can be used for SAT solving, namely for per-instance algorithm selection where there is a \u201cportfolio\u201d of SAT solvers and there is a \u201cmeta-solver\u201d that chooses a solver from the portfolio for a given input formula.<\/jats:p>","DOI":"10.3233\/sat-220006","type":"journal-article","created":{"date-parts":[[2023,1,6]],"date-time":"2023-01-06T12:14:01Z","timestamp":1673007241000},"page":"1-15","source":"Crossref","is-referenced-by-count":0,"title":["An Isomorphism-Invariant Distance Function on Propositional Formulas in CNF"],"prefix":"10.1177","volume":"14","author":[{"given":"Evgeny","family":"Dantsin","sequence":"first","affiliation":[{"name":"Department of Computer Science, Roosevelt University, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Wolpert","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Roosevelt University, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2023,1,4]]},"reference":[{"issue":"4","key":"10.3233\/SAT-220006_ref1","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1007\/s00453-008-9180-4","article-title":"Approximation algorithms for treewidth","volume":"56","author":"Amir","year":"2010","journal-title":"Algorithmica"},{"key":"10.3233\/SAT-220006_ref2","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.jal.2016.11.004","article-title":"Structure features for SAT instances classification","volume":"23","author":"Ans\u00f3tegui","year":"2017","journal-title":"Journal of Applied Logic"},{"key":"10.3233\/SAT-220006_ref3","unstructured":"G.\u00a0Ausiello, F.\u00a0Cristiano, P.\u00a0Fantozzi and L.\u00a0Laura, Syntactic isomorphism of CNF Boolean formulas is graph isomorphism complete, in: Proceedings of the 21st Italian Conference on Theoretical Computer Science, 2020, CEUR Workshop Proceedings, Vol.\u00a02756, CEUR-WS.org, 2020, pp.\u00a0190\u2013201."},{"key":"10.3233\/SAT-220006_ref4","doi-asserted-by":"crossref","unstructured":"L.\u00a0Babai, Graph isomorphism in quasipolynomial time [extended abstract], in: Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2016, ACM, 2016, pp.\u00a0684\u2013697.","DOI":"10.1145\/2897518.2897542"},{"key":"10.3233\/SAT-220006_ref5","doi-asserted-by":"crossref","unstructured":"D.\u00a0Burago, Y.\u00a0Burago and S.\u00a0Ivanov, A Course in Metric Geometry, Graduate Studies in Mathematics, Vol.\u00a033, American Mathematical Society, 2001.","DOI":"10.1090\/gsm\/033"},{"key":"10.3233\/SAT-220006_ref6","doi-asserted-by":"crossref","unstructured":"M.\u00a0Cygan, F.V.\u00a0Fomin, L.\u00a0Kowalik, D.\u00a0Lokshtanov, D.\u00a0Marx, M.\u00a0Pilipczuk, M.\u00a0Pilipczuk and S.\u00a0Saurabh, Parameterized Algorithms, Springer, 2015.","DOI":"10.1007\/978-3-319-21275-3"},{"issue":"1","key":"10.3233\/SAT-220006_ref7","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/S0304-3975(01)00337-1","article-title":"Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference","volume":"289","author":"Fleischner","year":"2002","journal-title":"Theoretical Computer Science"},{"issue":"2\u20133","key":"10.3233\/SAT-220006_ref8","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0166-218X(01)00358-4","article-title":"A perspective on certain polynomial-time solvable classes of satisfiability","volume":"125","author":"Franco","year":"2003","journal-title":"Discrete Applied Mathematics"},{"key":"10.3233\/SAT-220006_ref9","unstructured":"C.P.\u00a0Gomes, A.\u00a0Sabharwal and B.\u00a0Selman, Model counting, in: Handbook of Satisfiability, 2nd edn, Frontiers in Artificial Intelligence and Applications, Vol.\u00a0336, IOS Press, 2021, pp.\u00a0993\u20131014, Chapter 25."},{"key":"10.3233\/SAT-220006_ref10","unstructured":"M.\u00a0Gromov, Metric Structures for Riemannian and Non-Riemannian Spaces, Progress in Mathematics, Vol.\u00a0152, Birkh\u00e4user, 1999, Based on the 1981 French original."},{"key":"10.3233\/SAT-220006_ref11","doi-asserted-by":"crossref","unstructured":"H.H.\u00a0Hoos, F.\u00a0Hutter and K.\u00a0Leyton-Brown, Automated configuration and selection of SAT solvers, in: Handbook of Satisfiability, 2nd edn, Frontiers in Artificial Intelligence and Applications, Vol.\u00a0336, IOS Press, 2021, pp.\u00a0481\u2013507, Chapter 12.","DOI":"10.3233\/FAIA200995"},{"key":"10.3233\/SAT-220006_ref12","doi-asserted-by":"crossref","unstructured":"J.\u00a0K\u00f6bler, U.\u00a0Sch\u00f6ning and J.\u00a0Tor\u00e1n, The Graph Isomorphism Problem: Its Structural Complexity, Progress in Theoretical Computer Science, Birkh\u00e4user\/Springer, 1993.","DOI":"10.1007\/978-1-4612-0333-9"},{"key":"10.3233\/SAT-220006_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-80223-3_25"},{"key":"10.3233\/SAT-220006_ref14","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1016\/j.jsc.2013.09.003","article-title":"Practical graph isomorphism, II","volume":"60","author":"McKay","year":"2014","journal-title":"Journal of Symbolic Computation"},{"key":"10.3233\/SAT-220006_ref15","doi-asserted-by":"crossref","unstructured":"M.\u00a0Samer and S.\u00a0Szeider, Fixed-parameter tractability, in: Handbook of Satisfiability, 2nd edn, Frontiers in Artificial Intelligence and Applications, Vol.\u00a0336, IOS Press, 2021, pp.\u00a0693\u2013736, Chapter 17.","DOI":"10.3233\/FAIA201000"},{"key":"10.3233\/SAT-220006_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51825-7_19"},{"issue":"4","key":"10.3233\/SAT-220006_ref17","doi-asserted-by":"publisher","first-page":"656","DOI":"10.1016\/j.jcss.2004.04.009","article-title":"Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable","volume":"69","author":"Szeider","year":"2004","journal-title":"Journal of Computer and System Sciences"}],"container-title":["Journal on Satisfiability, Boolean Modeling and Computation"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/SAT-220006","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T07:08:26Z","timestamp":1761548906000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/SAT-220006"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,4]]},"references-count":17,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2023,1,4]]}},"URL":"https:\/\/doi.org\/10.3233\/sat-220006","relation":{},"ISSN":["1574-0617"],"issn-type":[{"type":"electronic","value":"1574-0617"}],"subject":[],"published":{"date-parts":[[2023,1,4]]}}}