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

TL;DR

This paper introduces a SAT-based method using the URSA system for developing, analyzing, and verifying reductions between NP-complete problems, enhancing the process with specialized features.

Contribution

It presents a novel SAT-based framework for the specification, analysis, and justification of NP-complete problem reductions, leveraging the URSA constraint solver.

Findings

Demonstrates the effectiveness of the URSA system in reduction verification

Provides a new formal approach for NP-complete problem reductions

Enhances reliability of reductions through SAT-based analysis

Abstract

We propose a novel approach for the development, analysis, and verification of reductions between NP-complete problems. This method uses the URSA system, a SAT-based constraint solver and incorporates features that distinguish it from existing related systems.