2SATsolver

Lists K solutions of a 2 SAT instance, having a minimum Hamming distance between them.

All binaries can be compiled with make and a brief test suite is available with make test. Below you will find the details about each available binary.

Example

Example Compilation

Compile the example with:

nvcc -Xcompiler -fopenmp -lgomp -Iinclude src/main.cu -o bin/main

Example Usage

Run the example with:

bin/main [-c] [-v] <test_file> <number of solutions> <minimum hamming distance>

• The -c flag is used to run the serial algorithm after the parallel one, then compare the execution times.
• The -v flag is used to print the solutions.

Many test files can be found in the test_data directory. Using the same binary file, you can test every file in the test_data directory using the script test_all.sh.

Instance generator

This program reads a 2 SAT instance from a text file, The file should contain one clause per line. Letters are represented by numbers from 0 to N, with the requirement that each number in this range must appear at least once. Negations are represented by prefixing the character "_".

An instance generated by this program is not guaranteed to be solvable, it only satisfies the above requirements.

Instance generator Compilation

Compile the generator with:

nvcc 2cnf_generator/2cnf_generator.cu -o bin/gen

Instance generator Usage

Run the generator with:

bin/gen <number of formulas> <probability of new variable> <output filename>

Benchmark

You can evaluate the performance of the solution generation algorithm under various configurations.

Benchmark Compilation

Compile the benchmark with:

nvcc -Xcompiler -fopenmp -lgomp -Iinclude src/benchmark.cu -o bin/benchmark

Benchmark Usage

Run the benchmark with:

bin/benchmark <repetitions number> <solutions number> <formulas per instance> <minimum distance between solutions> <probability to generate new variables> <parallel=1, serial=0> <output filename> [inputpath1 inputpath2 ...]

• <repetitions number>: Number of times to repeat the benchmark.
• <solutions number>: Number of solutions to generate per repetition.
• <formulas per instance>: Number of formulas per instance.
• <minimum distance between solutions>: Minimum Hamming distance between generated solutions.
• <probability to generate new variables>: Probability (0.0–1.0) to introduce new variables in formulas.
• <parallel=1, serial=0>: Set to 1 for parallel execution (GPU), 0 for serial execution (CPU).
• <output filename>: Path to the file where benchmark results will be saved.
• [inputpaths...]: List of paths to files containing 2sat formulas. If provided, the benchmark will iterate over the list, without creating new formulas. It can also be a directory, in such case all .txt files inside it will be used in the benchmark.

Adjust these parameters as needed to evaluate different scenarios and performance characteristics.