MiniSat Fork - An Enhanced SAT Solver

This repository contains a fork of the MiniSat SAT solver, developed as part of a project to analyze, understand, and optimize the tool for solving SAT problems. The project also includes benchmark tests, UML diagrams, and updated documentation for a deeper insight into MiniSat's functionalities.

Overview
MiniSat is a minimalistic yet highly efficient SAT solver widely used in both academic research and practical applications. This project extends and documents its functionalities with a focus on understanding its core algorithm—Conflict-Driven Clause Learning (CDCL)—and exploring performance optimizations.

Features
- Enhanced Documentation: Includes detailed comments within the codebase and a comprehensive technical report.
- Benchmark Results: Performance data for various SAT problems from the SAT Competition 2024 benchmarks.
- UML Diagrams: Visual representation of data flows and architectural structure.
- Improved Readability: Clarified setup instructions and code organization for ease of use.

Repository Structure
- `Benchmarks/`: Contains results of benchmarks, along with machine specifications used for testing.
- `Diagrams/`: UML diagrams visualizing key components and workflows.
- `Latex overleaf/`: Source files for the technical report.
- `README.md`: This document.
-  `minisat/`: Source code of MiniSat, with updated documentation and comments.
- `minisat/mtl/` :Mini Template Library
- `minisat/utils/`:Generic helper code (I/O, Parsing, CPU-time, etc)
- `minisat/core/` : A core version of the solver
- `minisat/simp/` : An extended solver with simplification capabilities
- `doc/` Documentation
- `LICENSE`: License information (MIT).

Installation Guide
To install and run MiniSat, follow these steps:

Prerequisites
- Operating System: Linux, macOS, or Windows (via WSL or MinGW).
- Dependencies: A  compiler 
Steps
1. Clone this repository:
   ```bash
   git clone https://github.com/aprecup14/minisat.git
   cd minisat
make
./minisat benchmarks/sample.cnf

Usage
To use MiniSat with a custom SAT problem:

Prepare your problem in DIMACS CNF format.
Run the solver with:
./minisat <input_file.cnf> <output_file.txt>
Check the output for satisfiability results.

 How to debug:

- When debugging it is important to run the `make install` command with the `CXXFLAGS` parameter set to `"-g -O0"`. This disables build optimizations for debugging, so that all the methods are accesible in debug mode. A `make clean` might be required before performing the `make install cr CXXFLAGS="-g -O0 -fpermissive"` to make sure changes are applied if the project was previously built.

- For VS Code users. A `.vscode` directory needs to be created. Inside it, a `launch.json` file has to be created to configure the debugger. Example of such a file:
```json{
    "version": "0.2.0",
    "configurations": [
        {
            "name": "Debug Project",
            "type": "cppdbg",
            "request": "launch",
            "program": "{PATH_TO_MINISAT_DIRECTORY}/build/release/bin/minisat_core", 
            "args": ["{PATH_TO_INPUT_FILE}", {PATH_OUTPUT_FILE}], // Add any command-line arguments if needed
            "stopAtEntry": false,
            "cwd": "${workspaceFolder}",
            "environment": [],
            "externalConsole": false,
            "MIMode": "gdb", // Use "lldb" for macOS or "cppvsdbg" for Windows
            "setupCommands": [
                {
                    "description": "Enable pretty-printing for gdb",
                    "text": "-enable-pretty-printing",
                    "ignoreFailures": true
                }
            ],
            "preLaunchTask": "build" // Optionally set to run `make` before debugging
        }
    ]
}```