LIPIcs.MFCS.2024.56.pdf
- Filesize: 0.78 MB
- 14 pages
Document
Specification and Automatic Verification of Computational Reductions
Authors
Julien Grange 
,
Fabian Vehlken ,
Nils Vortmeier ,
Thomas Zeume
-
Part of:
Volume:
49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Mathematical Foundations of Computer Science (MFCS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-08-23
File
Document Identifiers
Author Details
Cite As Get BibTex
Julien Grange, Fabian Vehlken, Nils Vortmeier, and Thomas Zeume. Specification and Automatic Verification of Computational Reductions. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 56:1-56:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.MFCS.2024.56
Abstract
We are interested in the following validation problem for computational reductions: for algorithmic problems P and P^⋆, is a given candidate reduction indeed a reduction from P to P^⋆? Unsurprisingly, this problem is undecidable even for very restricted classes of reductions. This leads to the question: Is there a natural, expressive class of reductions for which the validation problem can be attacked algorithmically? We answer this question positively by introducing an easy-to-use graphical specification mechanism for computational reductions, called cookbook reductions. We show that cookbook reductions are sufficiently expressive to cover many classical graph reductions and expressive enough so that SAT remains NP-complete (in the presence of a linear order). Surprisingly, the validation problem is decidable for natural and expressive subclasses of cookbook reductions.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic
- Theory of computation → Problems, reductions and completeness
Keywords
- Computational reductions
- automatic verification
- decidability
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Libor Barto, Jakub Opršal, and Michael Pinsker. The wonderland of reflections. Israel Journal of Mathematics, 223:363-398, 2018.
-
Manuel Bodirsky. Complexity of Infinite-Domain Constraint Satisfaction. Lecture Notes in Logic. Cambridge University Press, 2021.
- Michael S. Crouch, Neil Immerman, and J. Eliot B. Moss. Finding reductions automatically. In Andreas Blass, Nachum Dershowitz, and Wolfgang Reisig, editors, Fields of Logic and Computation, Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, volume 6300 of Lecture Notes in Computer Science, pages 181-200. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15025-8_10.
- Elias Dahlhaus. Reduction to NP-complete problems by interpretations. In Egon Börger, Gisbert Hasenjaeger, and Dieter Rödding, editors, Logic and Machines: Decision Problems and Complexity, Proceedings of the Symposium "Rekursive Kombinatorik" held from May 23-28, 1983 at the Institut für Mathematische Logik und Grundlagenforschung der Universität Münster/Westfalen, volume 171 of Lecture Notes in Computer Science, pages 357-365. Springer, 1983. URL: https://doi.org/10.1007/3-540-13331-3_51.
- Victor Dalmau and Jakub Oprsal. Local consistency as a reduction between constraint satisfaction problems. CoRR, abs/2301.05084, 2023. URL: https://doi.org/10.48550/arXiv.2301.05084.
-
Michael R Garey and David S Johnson. Computers and intractability, volume 174. freeman San Francisco, 1979.
- Neil Immerman. Languages that capture complexity classes. SIAM J. Comput., 16(4):760-778, 1987. URL: https://doi.org/10.1137/0216051.
- Neil Immerman. Descriptive complexity. Graduate texts in computer science. Springer, 1999. URL: https://doi.org/10.1007/978-1-4612-0539-5.
- Charles Jordan and Lukasz Kaiser. Experiments with reduction finding. In Matti Järvisalo and Allen Van Gelder, editors, Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings, volume 7962 of Lecture Notes in Computer Science, pages 192-207. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_15.
-
Leonid Libkin. Elements of finite model theory, volume 41. Springer, 2004.
- Marko Schmellenkamp, Fabian Vehlken, and Thomas Zeume. Teaching formal foundations of computer science with Iltis. Educational Column of the Bulletin of EATCS, 2024. URL: http://bulletin.eatcs.org/index.php/beatcs/article/download/797/842.