Merge branch 'main' of git@github.com:bearycool11/pmll.git

3-SAT.c

@@ -0,0 +1,33 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <time.h>
+
+// Function to generate a random 3-SAT instance
+void generate_3sat_instance(int num_variables, int num_clauses, const char* filename) {
+    FILE *file = fopen(filename, "w");
+    if (!file) {
+        perror("Failed to open file for writing");
+        return;
+    }
+
+    // Write the header for the 3-SAT CNF instance
+    fprintf(file, "p cnf %d %d\n", num_variables, num_clauses);
+
+    // Randomly generate clauses
+    srand(time(0));  // Seed the random number generator
+
+    for (int i = 0; i < num_clauses; ++i) {
+        // Each clause consists of 3 literals, choose them randomly
+        for (int j = 0; j < 3; ++j) {
+            int var = rand() % num_variables + 1;  // Variable between 1 and num_variables
+            if (rand() % 2 == 0) {
+                var = -var;  // Randomly negate the variable
+            }
+            fprintf(file, "%d ", var);
+        }
+        fprintf(file, "0\n");  // End of clause
+    }
+
+    fclose(file);
+    printf("Generated random 3-SAT instance: %s\n", filename);
+}

MAKEFILE

@@ -1,17 +1,31 @@
-CC = gcc
-CFLAGS = -Wall -Werror -std=c11 -pedantic -Wextra
-LDFLAGS = -lpthread -lcrypto -lssl -lcblas -fopenmp
-INCLUDES = -I./include
+# Specify the SAT test target and dependencies
+TARGETS = pmll arc_agi_benchmark pmll_np_solver sat_test
 
-ARC_AGI_BENCHMARK_CFLAGS = -DARC_AGI_BENCHMARK
-ARC_AGI_BENCHMARK_LDFLAGS = -larc_agi_benchmark
+# SAT Test target
+sat_test: SAT_Compare.o Pmll_NP_Solver.o MiniSAT.o generate_3sat_instance.o SAT_Solver.o
+	$(CC) $(CFLAGS) $(LDFLAGS) $(INCLUDES) -o $@ $^
 
-TARGETS = pmll arc_agi_benchmark pmll_np_solver
+# Compile SAT_Compare.o from SAT_Compare.c
+SAT_Compare.o: SAT_Compare.c SAT_Solver.h Pmll_NP_Solver.h MiniSAT.h
+	$(CC) $(CFLAGS) $(INCLUDES) -c $<
 
-.PHONY: all clean run run_arc_agi_benchmark run_pmll_np_solver
+# Compile MiniSAT.o from MiniSAT.c
+MiniSAT.o: MiniSAT.c MiniSAT.h
+	$(CC) $(CFLAGS) $(INCLUDES) -c $<
 
-all: $(TARGETS)
+# Compile Pmll_NP_Solver.o from Pmll_NP_Solver.c
+Pmll_NP_Solver.o: Pmll_NP_Solver.c Pmll_NP_Solver.h
+	$(CC) $(CFLAGS) $(INCLUDES) -c $<
 
+# Compile SAT_Solver.o from SAT_Solver.c
+SAT_Solver.o: SAT_Solver.c SAT_Solver.h
+	$(CC) $(CFLAGS) $(INCLUDES) -c $<
+
+# Compile generate_3sat_instance.o from 3-SAT.c (used for SAT instance generation)
+generate_3sat_instance.o: 3-SAT.c SAT_Solver.h
+	$(CC) $(CFLAGS) $(INCLUDES) -c $<
+
+# Existing targets
 pmll: unified_voice.o pml_logic_loop.o memory_silo.o io_socket.o persistence.o main.o
 	$(CC) $(CFLAGS) $(LDFLAGS) $(INCLUDES) -o $@ $^
 
@@ -21,6 +35,7 @@ pmll_np_solver: pmll_np_solver.o
 arc_agi_benchmark: arc_agi_benchmark.o
 	$(CC) $(CFLAGS) $(ARC_AGI_BENCHMARK_CFLAGS) $(LDFLAGS) $(ARC_AGI_BENCHMARK_LDFLAGS) $(INCLUDES) -o $@ $^
 
+# Compilation rules for other .o files
 unified_voice.o: unified_voice.c memory_silo.h io_socket.h
 	$(CC) $(CFLAGS) $(INCLUDES) -c $<
 
@@ -42,12 +57,14 @@ main.o: main.c
 arc_agi_benchmark.o: arc_agi_benchmark.c
 	$(CC) $(CFLAGS) $(ARC_AGI_BENCHMARK_CFLAGS) $(INCLUDES) -c $<
 
-pmll_np_solver.o: pmll_np_solver.c
+pmll_np_solver.o: Pmll_NP_Solver.c
 	$(CC) $(CFLAGS) $(INCLUDES) -c $<
 
+# Clean up
 clean:
 	rm -f *.o $(TARGETS)
 
+# Run commands
 run: pmll
 	./pmll
 
@@ -56,3 +73,7 @@ run_arc_agi_benchmark: arc_agi_benchmark
 
 run_pmll_np_solver: pmll_np_solver
 	./pmll_np_solver
+
+# Add a run command for the SAT test
+run_sat_test: sat_test
+	./sat_test

MiniSAT.c

@@ -0,0 +1,37 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <time.h>
+
+// Function to run the external MiniSat solver with performance logging
+void run_miniSat(const char* filename, FILE *log_file) {
+    // Start measuring the execution time of MiniSat
+    clock_t start_time = clock();
+
+    char command[256];
+    sprintf(command, "minisat %s result.txt", filename);  // Assuming 'minisat' is in the system path
+    int result = system(command);
+
+    // End measuring the execution time of MiniSat
+    clock_t end_time = clock();
+    double miniSat_time = (double)(end_time - start_time) / CLOCKS_PER_SEC;
+
+    // Read the result from the result.txt file generated by MiniSat
+    FILE *result_file = fopen("result.txt", "r");
+    if (!result_file) {
+        perror("Failed to open result file");
+        return;
+    }
+
+    char result_str[20];
+    fgets(result_str, sizeof(result_str), result_file);
+    if (strstr(result_str, "SATISFIABLE") != NULL) {
+        fprintf(log_file, "MiniSat: Satisfiable (Time: %.4f seconds)\n", miniSat_time);
+        printf("MiniSat: Satisfiable\n");
+    } else {
+        fprintf(log_file, "MiniSat: Unsatisfiable (Time: %.4f seconds)\n", miniSat_time);
+        printf("MiniSat: Unsatisfiable\n");
+    }
+
+    fclose(result_file);
+}

PMLL_SAT_Solver.c

@@ -0,0 +1,66 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <stdbool.h>
+#include <time.h>
+
+// Function to evaluate a CNF formula with a given variable assignment
+bool evaluate_formula(int **formula, int *assignment, int num_clauses, int num_variables) {
+    for (int i = 0; i < num_clauses; i++) {
+        bool clause_satisfied = false;
+        for (int j = 0; j < 3; j++) {
+            int var = formula[i][j];
+            if (var > 0 && assignment[var - 1] == 1) {
+                clause_satisfied = true;
+                break;
+            }
+            if (var < 0 && assignment[-var - 1] == 0) {
+                clause_satisfied = true;
+                break;
+            }
+        }
+        if (!clause_satisfied) {
+            return false;  // If one clause is not satisfied, formula is unsatisfied
+        }
+    }
+    return true;  // If all clauses are satisfied
+}
+
+// Backtracking solver using the PMLL algorithm with performance tracking
+bool PMLL_SAT_Solver(int **formula, int num_clauses, int num_variables, FILE *log_file) {
+    int *assignment = (int *)calloc(num_variables, sizeof(int));  // All variables are initially unassigned (0)
+    int iterations = 0;
+    int backtracks = 0;
+    clock_t start_time = clock();
+
+    // Recursive backtracking
+    for (int i = 0; i < num_variables; ++i) {
+        assignment[i] = 1;  // Try true (1)
+        iterations++;
+        if (evaluate_formula(formula, assignment, num_clauses, num_variables)) {
+            // Log data after finding a solution
+            clock_t end_time = clock();
+            fprintf(log_file, "PMLL Algorithm: Satisfiable (Time: %.4f seconds, Iterations: %d, Backtracks: %d)\n",
+                    (double)(end_time - start_time) / CLOCKS_PER_SEC, iterations, backtracks);
+            free(assignment);
+            return true;
+        }
+        assignment[i] = 0;  // Try false (0)
+        iterations++;
+        if (evaluate_formula(formula, assignment, num_clauses, num_variables)) {
+            // Log data after finding a solution
+            clock_t end_time = clock();
+            fprintf(log_file, "PMLL Algorithm: Satisfiable (Time: %.4f seconds, Iterations: %d, Backtracks: %d)\n",
+                    (double)(end_time - start_time) / CLOCKS_PER_SEC, iterations, backtracks);
+            free(assignment);
+            return true;
+        }
+        backtracks++;  // Count backtracks
+    }
+
+    // If no assignment satisfies the formula, return unsatisfiable
+    clock_t end_time = clock();
+    fprintf(log_file, "PMLL Algorithm: Unsatisfiable (Time: %.4f seconds, Iterations: %d, Backtracks: %d)\n",
+            (double)(end_time - start_time) / CLOCKS_PER_SEC, iterations, backtracks);
+    free(assignment);
+    return false;
+}