A SAT-based Approach for Specification, Analysis, and Justification of Reductions between NP-complete Problems

2025/11/23 by Janičić, Predrag
Computer Science · #Constraint Satisfaction and Optimization #Formal Methods in Verification #Logic, Reasoning, and Knowledge

paper · doi:10.48550/arxiv.2511.18639

Abstract

We propose a novel framework for developing, analyzing, and validating reductions between NP-complete problems. Powered by the SAT-based constraint solver URSA, our methodology introduces several distinct features that set it apart from other related approaches. The proposed workflow effectively bridges the crucial gap between informal, high-level reduction descriptions and formalized mathematical proofs. By supplementing rather than replacing human intuition, this interactive methodology serves as an aid for exploring relationships between NP-complete problems.

Citations

• Thermodynamic Limits of Proof
• Tool-Assisted Learning of Computational Reductions
• Specification and Automatic Verification of Computational Reductions
• Verification of NP-hardness Reduction Functions for Exact Lattice Problems

Related

• A simple way to reduce factorization problems to SAT
• Structural Origin and the Minimal Syntax of NP-Hardness: Analysis of SAT from Syntactic Generativity and Compositional Collapse
• Set Constraint Model and Automated Encoding into SAT: Application to the\n Social Golfer Problem
• From k-SAT to k-CSP: Two Generalized Algorithms
• SAT vs CSP: a commentary