Non-deterministic Processor (NDP) - Parallel SAT-Solver with OpenMP

This NDP is an efficient parallel SAT-Solver. It parses DIMACS, factorizes, and performs parallel searches using BFS (Breadth-First Search) and DFS (Depth-First Search) techniques.
NDP 4.5.7 supports custom configuration through command-line options, utilizes multi-threading via OpenMP, and outputs results to a dynamically generated file name based on the input parameters saving results to a dynamically generated file name based on the input parameters and the current UTC time. Version 4.5.7 now with with Profiling.

NDP-4_5_7.cpp IPFS CID: QmTFJ9PXHDxf7hPYBJbQo7azpwAocXjj1e91gjosWg5Dwh
ClauseSetPool.hpp IPFS CID: QmSyx6AiarRDKVs2LRUQivtnjiUiYpbqvA39odWujd7Pep

Requirements

Input

• Generate DIMACS files at Paul Purdom and Amr Sabry's CNF Generator:
  Paul Purdom's CNF Generator
• For bit-wise input generation, use:
  RSA Challenge
• Input file extensions: any & none E.g: .dimacs ⎪ .cnf ⎪ .txt ⎪ .doc ⎪ .xyz ⎪ [filname]
• Generate DIMACS locally:
  CNF_FACT-MULT
• Or on IPFS: ipfs://QmYuzG46RnjhVXQj7sxficdRX2tUbzcTkSjZAKENMF5jba

GMP Library

GMP (GNU Multiple Precision Arithmetic Library) to handle big numbers and verify the results.

OpenMP:

Required for distributed computation across nodes.

Install with:

sudo apt install g++ libgmp-dev libgmpxx4ldbl libomp-dev

Compilation

Ensure you have at least GCC 9+, preferably GCC 11 or 12):

g++ --version

Ensure to have ClauseSetPool.hpp in the working directory.

To compile the program on Linux (tested on Ubuntu 24.04.1 LTS), use the following command:

g++ -fopenmp -std=c++17 -Ofast -march=native -mtune=native -fomit-frame-pointer -funroll-loops -fprefetch-loop-arrays -flto=auto -ffast-math -static-libgcc -static-libstdc++ -o NDP-4_5_7 NDP-4_5_7.cpp -lgmpxx -lgmp -lstdc++fs

CLI usage

Once compiled, the program can be run from the command line using the following format:

./NDP-4_5_7 <dimacs_file> [-d depth | -t max_tasks | -q max_queue_size | -r reserved cores] [-o output_directory]

Command-Line Options:

<dimacs_file>: The path to the input DIMACS file.
-d depth: Set a custom depth for BFS iterations. (Optional)
-t max_tasks: Set the maximum number of tasks for BFS. (Optional)
-q max_queues: Limit the maximum number of tasks in the BFS queue. (Optional)
-r reserve_cores: Reserve a certain number of CPU cores for the system, reducing the number of cores used by the program. (Optional)
-o output_directory: Specify a custom output directory for the result files. (Optional)

Basic execution with nodes (example):
Basic execution: ./NDP-4_5_7 inputs/RSA/rsaFACT-24bit.dimacs

This will run the program using the default settings for BFS and DFS and output the results to the current working directory.

Defaults:

max_tasks = num_clauses - num_vars

Reserved Cores = 0

output_directory = input_directory

Customization:

Setting a custom depth: ./NDP-4_5_7 inputs/RSA/rsaFACT-24bit.dimacs -d 5000

Limiting the number of tasks: ./NDP-4_5_7 inputs/RSA/rsaFACT-24bit.dimacs -t 1000

Setting a custom Queue Size: ./NDP-4_5_7 inputs/RSA/rsaFACT-24bit.dimacs -q 256

Saving results to a specific directory: ./NDP-4_5_7 inputs/RSA/rsaFACT-24bit.dimacs -o /path/to/output

Monitoring

Monitor system and CPU usage on each node in real time:

htop

Output

The output file will be saved in the format: NDP-4_5_7_rsaFACT13688e7-24bit_8dfcb_auto_r0.txt
(no cli option for Depth/#Tasks/Queue Size, no reserved cores)

NOTE:

only accepts input generated by Paul Purdom's CNF Generator - for code comments and any assistance paste code into ChatGPT and/or contact GridSAT Stiftung