Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Predrag Janičić

TL;DR

This work addresses the challenge of designing, analyzing, and justifying reductions between $\mathsf{NP}$-complete problems by leveraging URSA, a SAT-based constraint solver. The authors show how to represent problem instances, certificate verification, and reductions within a single framework, enabling solving, composition of reductions, and bounded-size automatic verification through equisatisfiability and certificate linkage. Key contributions include a general URSA-based methodology for reductions, concrete demonstrations such as $k$-clique to $l$-vertex-cover and $3$-SAT to $3$-coloring, and the demonstration that reductions can be automatically verified for given instance sizes, providing rapid prototyping and justification of reductions. The approach offers a practical, extensible toolkit for education and research to prototype and test reductions, while acknowledging that these verifications are not full formal proofs and may benefit from integration with proof assistants for complete formalization.

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.

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

TL;DR

This work addresses the challenge of designing, analyzing, and justifying reductions between -complete problems by leveraging URSA, a SAT-based constraint solver. The authors show how to represent problem instances, certificate verification, and reductions within a single framework, enabling solving, composition of reductions, and bounded-size automatic verification through equisatisfiability and certificate linkage. Key contributions include a general URSA-based methodology for reductions, concrete demonstrations such as -clique to -vertex-cover and -SAT to -coloring, and the demonstration that reductions can be automatically verified for given instance sizes, providing rapid prototyping and justification of reductions. The approach offers a practical, extensible toolkit for education and research to prototype and test reductions, while acknowledging that these verifications are not full formal proofs and may benefit from integration with proof assistants for complete formalization.

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.

Paper Structure

This paper contains 11 sections, 8 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Overview of the paper.
  3. Background
  4. np-completeness
  5. sat Problem and sat Solvers.
  6. System ursa
  7. Solving np-complete Problems using ursa
  8. Reductions between np-complete Problems using ursa
  9. Verification of Reductions between np-complete Problems using ursa
  10. Related Work
  11. Conclusions and Future Work

Figures (5)

  • Figure 1: Code for solving $k$-clique problem: verifying that a concrete certificate is correct (left) and finding a certificate for given instance (right)
  • Figure 2: Code for solving $l$-vertex cover problem
  • Figure 3: Code for $k$-cluque to $l$-vertex cover reduction
  • Figure 4: Code for $l$-vertex cover to $k$-cluque reduction
  • Figure 5: Code for verification of $k$-cluque to $l$-vertex cover reduction

Theorems & Definitions (10)

  • Example 2.1: Clique to Vertex Cover reduction
  • Example 2.2
  • Example 2.3
  • Example 3.1: $k$-clique solver
  • Example 3.2: $l$-vertex cover solver
  • Example 4.1: $k$-clique to $l$-vertex cover reduction
  • Example 4.2: $l$-vertex cover to $k$-clique reduction
  • Example 5.1: verification of $k$-clique to $l$-vertex cover reduction
  • Example 5.2: verification of 3 sat to 3colouring reduction
  • Example 5.3: verification of sat to 3 sat reduction