Algorithmic Complexity Project: SAT, 3-SAT, and SUBSETSUM

Introduction

This project provides a comprehensive study of three fundamental NP-complete problems: SAT (Boolean Satisfiability), 3-SAT, and SUBSETSUM. The repository contains implementations for solving, verifying, and analyzing these problems, along with algorithmic reductions between them. The primary goal is to study their time and space complexity through both theoretical analysis and empirical benchmarking.

Table of Contents

• Introduction
• Project Overview
• Repository Structure
• Installation
• Usage Guide
  • Automated Execution
  • Manual Execution
  • Benchmarks
• Algorithmic Approach
  • Solvers
  • Reductions
• Results and Analysis

Project Overview

This project explores the complexity classes of NP-complete problems by implementing:

1. Solvers: Exact algorithms (Brute Force) to find solutions for SAT, 3-SAT, and SUBSETSUM.
2. Verifiers: Polynomial-time algorithms to verify the correctness of a given solution.
3. Reductions: Algorithms to transform instances of one problem into another:
   • SAT $\rightarrow$ 3-SAT
   • SAT $\rightarrow$ SUBSETSUM
4. Benchmarks: Extensive performance testing on generated instances and standard libraries (SATLIB).

Repository Structure

The project is organized as follows:

.
├── main.py                         # Main entry point for the project
├── structures.py                   # Data structures (Literal, Clause, Instances)
├── generation_instances.py         # Script to generate random problem instances
├── Benchmarks/                     # Benchmarking scripts and results
│   ├── Libs/                       # Benchmarks on standard libraries (SATLIB)
│   └── Local/                      # Benchmarks on locally generated instances
├── trouve_sol_SAT.py               # Solver for SAT
├── trouve_sol_3SAT.py              # Solver for 3-SAT
├── trouve_sol_subsetsum.py         # Solver for SUBSETSUM
├── verification_sol_SAT.py         # Verifier for SAT
├── verification_sol_3SAT.py        # Verifier for 3-SAT
├── verification_sol_subsetsum.py   # Verifier for SUBSETSUM
├── reduction_SAT_3SAT.py           # Reduction algorithm: SAT to 3-SAT
├── reduction_sat_sabsetsum.py      # Reduction algorithm: SAT to SUBSETSUM
└── analyse_*.ipynb                 # Jupyter Notebooks for complexity analysis

Installation

Ensure you have Python 3.8+ installed. The project requires the following dependencies:

• pandas
• numpy
• matplotlib
• seaborn
• openpyxl

You can install the required packages using pip:

pip install pandas numpy matplotlib seaborn openpyxl

Usage Guide

Automated Execution

The easiest way to run the entire project pipeline (generation, benchmarking, and reporting) is via the main.py script.

python main.py --auto

This command will:

1. Verify the Python environment.
2. Generate DIMACS instances for SAT, 3-SAT, and SUBSETSUM.
3. Run benchmarks on the generated instances.
4. Generate Excel reports in Benchmarks/Local/machine_stats/.
5. Display a summary of the statistics.

Manual Execution

You can also run individual components of the project.

Generating Instances:

python generation_instances.py --dimacs

Running Standard Benchmarks (SATLIB):

python Benchmarks/Libs/satlib_benchmarks.py

Benchmarks

The project includes two types of benchmarks:

1. Local Benchmarks: Tests algorithms on randomly generated instances of increasing size to observe exponential growth.
2. Library Benchmarks: Tests algorithms on standard problem sets (e.g., SATLIB uf20-91) to validate correctness and performance against known standards.

Results are saved as Excel files in the Benchmarks/Local/machine_stats/ directory.

Algorithmic Approach

Solvers

The project implements Brute Force solvers for all three problems. These algorithms systematically explore the solution space:

• SAT / 3-SAT: Explores all $2^n$ possible truth assignments.
• SUBSETSUM: Explores all $2^n$ possible subsets.

While these algorithms guarantee finding a solution if one exists, they have an exponential time complexity of $O(2^n)$.

Reductions

The project demonstrates the NP-completeness of the problems by implementing polynomial-time reductions:

1. SAT $\rightarrow$ 3-SAT: Transforms any SAT formula into an equivalent 3-CNF formula. It handles clauses of varying lengths by introducing auxiliary variables to split them into clauses of exactly 3 literals.
2. SAT $\rightarrow$ SUBSETSUM: Transforms a SAT formula into a set of integers and a target sum. It constructs numbers in base-10 (or higher) where digits represent the satisfaction of clauses and the selection of variables.

Results and Analysis

Detailed analysis of the algorithms' performance is available in the Jupyter Notebooks:

• analyse_empirique_complete.ipynb: Comprehensive visualization of time and space complexity.
• analyse_complexite_SAT.ipynb: Specific analysis for SAT.
• analyse_complexite_3SAT.ipynb: Specific analysis for 3-SAT.
• analyse_complexite_SUBSETSUM.ipynb: Specific analysis for SUBSETSUM.

To view the analysis:

1. Open the desired notebook in VS Code or Jupyter Lab.
2. Run all cells to generate the graphs and statistics.