# SATLAB

**Repository Path**: marvintau/satlab

## Basic Information

- **Project Name**: SATLAB
- **Description**: A library for manipulating CNF in different forms for better dealing with SAT problem.
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2025-02-21
- **Last Updated**: 2025-08-07

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# SAT Problem Image Analysis

This repository contains tools for analyzing SAT problem visualizations using computer vision and machine learning techniques.

## Overview

The SAT Lab generates various visualizations of SAT problems:
- Original full-size images
- 256x256 and 128x128 scaled images
- Hough transform images that highlight linear patterns
- Subtracted Hough images that isolate non-linear components

This multi-scale approach helps identify structural patterns in SAT problems that might not be visible with a single visualization technique.

## Image Analysis Features

The `satlab_image_analysis.py` script:

1. **Multi-scale feature extraction**: Extracts features from different image sizes to capture different levels of detail
2. **Multiple neural networks**: Uses ResNet-18 for higher resolution images and MobileNet for smaller images
3. **Combined feature representation**: Concatenates features from all image types for a comprehensive representation
4. **Dimensionality reduction**: Applies PCA and t-SNE for visualization
5. **Multiple clustering approaches**: Tries various clustering algorithms (K-means, DBSCAN) with different parameters
6. **Hough pattern analysis**: Special analysis of linear patterns detected by the Hough transform

## Requirements

- Python 3.7+
- PyTorch 1.8+
- torchvision
- NumPy
- scikit-learn
- Matplotlib
- Pandas
- PIL (Pillow)

Install requirements with:
```
pip install torch torchvision numpy scikit-learn matplotlib pandas pillow
```

## Usage

The new CLI supports two main subcommands:

### Generate Scope Arrays

```
./satlab gen-scope <source CNF dir> <dest array dir> [--type=origin|sorted|all] [--db=meta.db]
```
- Parses all .cnf and .cnf.xz files in the source directory.
- Generates 512x512 scope array files for each instance.
- Output files are named: `<uuid>~<family>~origin.scope` and/or `<uuid>~<family>~sorted.scope`.
- `--type` (default: all):
    - `origin`: only original order
    - `sorted`: only sorted order
    - `all`: both
- `--db` (default: meta.db): Path to the SQLite database for family lookup.

**Example:**
```
./satlab gen-scope ./all-instance ./all-instance-scope --type=all
```

### Generate Images from Scope Arrays

```
./satlab gen-image <source array dir> <dest image dir> [--type=ident|fft2d|hough|morph|all]
```
- Reads all `.scope` files in the source array directory.
- Generates images for each scope array.
- Output files are named: `<uuid>~<family>~<kind>~<type>~512.bmp`
- `--type` (default: all):
    - `ident`: identity image
    - `fft2d`: FFT image
    - `hough`: Hough transform image
    - `morph`: Morphological image
    - `all`: all types

**Example:**
```
./satlab gen-image ./all-instance-scope ./all-instance-image --type=all
```

---

For batch processing, see `process_instances.sh` for parallelized scope generation.

## Interpreting Results

- **Similar SAT problems** will appear close together in the t-SNE visualization
- **Clusters** may represent problems with similar structural characteristics
- **Hough transform intensity** can indicate the presence of strong linear patterns in the problem structure

## Advanced Analysis

You can extend the analysis by:

1. Adding custom feature extractors for specific SAT problem characteristics
2. Using the extracted features for SAT solver selection or parameter tuning
3. Creating a supervised learning model if you have performance data for each SAT problem

## Troubleshooting

- **CUDA out of memory**: Reduce batch size or use CPU mode
- **Missing images**: Ensure all image types are present in the image directory
- **Poor clustering results**: Try different clustering parameters or feature extraction methods