Skip to content

Commit

Permalink
Create SAT_Compare.c
Browse files Browse the repository at this point in the history
Signed-off-by: Josef Edwards <joed6834@colorado.edu>
  • Loading branch information
bearycool11 authored Nov 13, 2024
1 parent e035883 commit 7bf66fd
Showing 1 changed file with 37 additions and 0 deletions.
37 changes: 37 additions & 0 deletions SAT_Compare.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
#include <stdio.h>
#include <stdlib.h>
#include <time.h>

// Test function to run the PMLL solver and MiniSat solver, and compare results
void run_tests(int num_variables, int num_clauses) {
char filename[256];
sprintf(filename, "3sat_instance_%d_%d.cnf", num_variables, num_clauses);

// Step 1: Generate random SAT instance
generate_3sat_instance(num_variables, num_clauses, filename);

// Step 2: Run the PMLL algorithm (SAT Solver)
clock_t start_time = clock();
int **formula = load_cnf(filename); // Load the generated CNF formula (to be implemented)
bool pml_result = PMLL_SAT_Solver(formula, num_clauses, num_variables);
clock_t end_time = clock();
double pml_time = (double)(end_time - start_time) / CLOCKS_PER_SEC;
printf("PMLL Algorithm: %s (Time: %f seconds)\n", pml_result ? "Satisfiable" : "Unsatisfiable", pml_time);

// Step 3: Run MiniSat solver and measure time
start_time = clock();
run_miniSat(filename);
end_time = clock();
double miniSat_time = (double)(end_time - start_time) / CLOCKS_PER_SEC;
printf("MiniSat: Time: %f seconds\n", miniSat_time);

// Free resources
free_formula(formula); // Implement memory cleanup
}

int main() {
int num_variables = 50;
int num_clauses = 150;
run_tests(num_variables, num_clauses);
return 0;
}

0 comments on commit 7bf66fd

Please sign in to comment.