An Isomorphism-Invariant Distance Function on Propositional Formulas in CNF

DOI10.3233/sat-220006zbMath1523.68044OpenAlexW4313650690MaRDI QIDQ6113549

Alexander Wolpert, Evgeny Dantsin

Publication date: 11 July 2023

Published in: Journal on Satisfiability, Boolean Modeling and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3233/sat-220006

zbMATH Keywords

isomorphism invariantsdistance on CNF formulasper-instance algorithm selection

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Classical propositional logic (03B05) Computational aspects of satisfiability (68R07)

Cites Work

• Unnamed Item
• Unnamed Item
• Approximation algorithms for treewidth
• Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• A perspective on certain polynomial-time solvable classes of satisfiability
• Practical graph isomorphism. II.
• A faster algorithm for propositional model counting parameterized by incidence treewidth
• Graph isomorphism in quasipolynomial time [extended abstract]
• Parameterized Algorithms
• Metric structures for Riemannian and non-Riemannian spaces. Transl. from the French by Sean Michael Bates. With appendices by M. Katz, P. Pansu, and S. Semmes. Edited by J. LaFontaine and P. Pansu