Verification of NP-Hardness Reduction Functions for Exact Lattice Problems

Katharina Kreuzer, Tobias Nipkow

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

This paper describes the formal verification of NP-hardness reduction functions of two key problems relevant in algebraic lattice theory: the closest vector problem and the shortest vector problem, both in the infinity norm. The formalization uncovered a number of problems with the existing proofs in the literature. The paper describes how these problems were corrected in the formalization. The work was carried out in the proof assistant Isabelle.

Original languageEnglish
Title of host publicationAutomated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings
EditorsBrigitte Pientka, Cesare Tinelli
PublisherSpringer Science and Business Media Deutschland GmbH
Pages365-381
Number of pages17
ISBN (Print)9783031384981
DOIs
StatePublished - 2023
EventProceedings of the 29th International Conference on Automated Deduction, CADE-29 - Rome, Italy
Duration: 1 Jul 20234 Jul 2023

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14132 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceProceedings of the 29th International Conference on Automated Deduction, CADE-29
Country/TerritoryItaly
CityRome
Period1/07/234/07/23

Keywords

  • NP-hardness
  • integer programming
  • lattice problems
  • verification

Fingerprint

Dive into the research topics of 'Verification of NP-Hardness Reduction Functions for Exact Lattice Problems'. Together they form a unique fingerprint.

Cite this