Specification and Automatic Verification of Computational Reductions

Grange, Julien; Vehlken, Fabian; Vortmeier, Nils; Zeume, Thomas

doi:10.4230/LIPIcs.MFCS.2024.56

File

LIPIcs.MFCS.2024.56.pdf

Filesize: 0.78 MB
14 pages

Document Identifiers

DOI: 10.4230/LIPIcs.MFCS.2024.56
URN: urn:nbn:de:0030-drops-206122

Author Details

Julien Grange

LACL, Université Paris-Est Créteil, France

Fabian Vehlken

Ruhr University Bochum, Germany

Nils Vortmeier

Ruhr University Bochum, Germany

Thomas Zeume

Ruhr University Bochum, Germany

Cite AsGet 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)

0

PDF Downloads

0

Metadata Views

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.