Codex-generated pull request by piyush-J · Pull Request #2 · piyush-J/AlphaMapleSAT

piyush-J · 2026-02-18T06:43:55Z

Codex generated this pull request, but encountered an unexpected error after generation. This is a placeholder PR message.

Codex Task

Copilot

Pull request overview

This PR introduces two C++ implementations of SAT solver cubing algorithms as lightweight demonstrations alongside the existing Python-based AlphaMapleSAT implementation. The changes add educational/demo code for MCTS-based cubing and beam lookahead variable selection strategies.

Changes:

Added simple_mcts.cpp implementing a Monte Carlo Tree Search (MCTS) approach for SAT variable assignment exploration and cube generation
Added beam_lookahead.cpp implementing a beam lookahead algorithm with depth-1 and depth-2 variable scoring for cube generation
Updated README.md with compilation instructions, usage examples, and algorithm descriptions for both new C++ implementations

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 22 comments.

File	Description
simple_mcts.cpp	New file implementing MCTS-based cubing with BCP routines, CNF parsing, variable scoring, and cube generation
beam_lookahead.cpp	New file implementing beam lookahead algorithm with risk-aware variable scoring using depth-1 and depth-2 signals
README.md	Added documentation sections for both C++ demo tools with build instructions and example usage

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-02-18T06:49:44Z

@@ -0,0 +1,665 @@
+#include <bits/stdc++.h>


Using #include <bits/stdc++.h> is non-standard and not portable. This header is a GCC-specific convenience header that includes most of the C++ standard library. For portable code, explicitly include only the required standard headers (e.g., , , , etc.).

Suggested change

#include <bits/stdc++.h>

Copilot · 2026-02-18T06:49:45Z

+                if (!ptr) break;
+                ptr++;
+            }
+            clauses[clause_index] = (int *)malloc(sizeof(int) * size);


Missing error handling for malloc failure. If malloc returns NULL, the subsequent memcpy will crash. Add a null check and appropriate error handling.

Suggested change

clauses[clause_index] = (int *)malloc(sizeof(int) * size);

clauses[clause_index] = (int *)malloc(sizeof(int) * size);

if (clauses[clause_index] == NULL) {

fprintf(stderr, "Out of memory while allocating clause.\n");

exit(1);

}

Copilot · 2026-02-18T06:49:45Z

@@ -0,0 +1,380 @@
+#include <bits/stdc++.h>


Using #include <bits/stdc++.h> is non-standard and not portable. This header is a GCC-specific convenience header that includes most of the C++ standard library. For portable code, explicitly include only the required standard headers.

Suggested change

#include <bits/stdc++.h>

#include <vector>

Copilot · 2026-02-18T06:49:45Z

+        exit(1);
+    }
+
+    char line[10000];


Potential buffer overflow: the line buffer is fixed at 10000 bytes. If a CNF file contains a line longer than 9999 characters (plus null terminator), this will cause undefined behavior. Consider using a dynamic buffer or larger fixed size with proper bounds checking.

Copilot · 2026-02-18T06:49:45Z

+            printf("        S2_mean=(%.3f+%.3f)/2=%.3f\n", s2_plus, s2_minus, s2_mean);
+            printf("        S2_balanced=%.3f - %.2f*|%.3f-%.3f| = %.3f\n",
+                   s2_mean, gamma, s2_plus, s2_minus, s2_balanced);
+        }
+    }
+
+    double max_s1 = 1e-9, max_s2 = 1e-9;
+    for (const auto& u : updated) {
+        max_s1 = max(max_s1, u.s1);
+        max_s2 = max(max_s2, u.s2_balanced);
+    }
+
+    for (auto& u : updated) {
+        u.s1_norm = u.s1 / max_s1;


Potential division by zero. If max_s1 or max_s2 remain at their initial value of 1e-9 (when all scores are zero or negative), the normalization on lines 318-319 could produce unexpected results. While 1e-9 prevents actual division by zero, consider adding explicit checks or handling for the case where all scores are zero.

Suggested change

printf(" S2_mean=(%.3f+%.3f)/2=%.3f\n", s2_plus, s2_minus, s2_mean);

printf(" S2_balanced=%.3f - %.2f*|%.3f-%.3f| = %.3f\n",

s2_mean, gamma, s2_plus, s2_minus, s2_balanced);

}

}

double max_s1 = 1e-9, max_s2 = 1e-9;

for (const auto& u : updated) {

max_s1 = max(max_s1, u.s1);

max_s2 = max(max_s2, u.s2_balanced);

}

for (auto& u : updated) {

u.s1_norm = u.s1 / max_s1;

double max_s1 = 0.0, max_s2 = 0.0;

for (const auto& u : updated) {

if (u.s1 > max_s1) {

max_s1 = u.s1;

}

if (u.s2_balanced > max_s2) {

max_s2 = u.s2_balanced;

}

}

const double norm_s1_den = (max_s1 > 0.0) ? max_s1 : 1.0;

const double norm_s2_den = (max_s2 > 0.0) ? max_s2 : 1.0;

for (auto& u : updated) {

u.s1_norm = (max_s1 > 0.0) ? (u.s1 / norm_s1_den) : 0.0;

u.s2_norm = (max_s2 > 0.0) ? (u.s2_balanced / norm_s2_den) : 0.0;

u.updated_score = (1.0 - lambda) * u.s1_norm + lambda * u.s2_norm;

if (debug) {

printf("\n[debug] normalize+combine for x=%d\n", u.seed_var);

printf(" S1_norm=%.3f/%.3f=%.6f\n", u.s1, norm_s1_den, u.s1_norm);

printf(" S2_norm=%.3f/%.3f=%.6f\n", u.s2_balanced, norm_s2_den, u.s2_norm);

Copilot · 2026-02-18T06:49:47Z

+#include <cstdio>
+#include <cstdlib>
+#include <cstring>
+#include <cstdint>
+


Redundant includes after #include <bits/stdc++.h>. Lines 4-7 include headers that are already included by bits/stdc++.h. Either remove the bits/stdc++.h include and keep explicit includes, or remove these redundant includes.

Suggested change

#include <cstdio>

#include <cstdlib>

#include <cstring>

#include <cstdint>

Copilot · 2026-02-18T06:49:48Z

+            clauses[clause_index] = (int*)malloc(sizeof(int) * size);
+            memcpy(clauses[clause_index], lits, sizeof(int) * size);


Potential memory leak: dynamically allocated clause arrays in the clauses array are never freed. Consider adding cleanup code or using RAII containers like std::vector instead of raw pointers to manage memory automatically.

Copilot · 2026-02-18T06:49:48Z

+            clauses[clause_index] = (int*)malloc(sizeof(int) * size);
+            memcpy(clauses[clause_index], lits, sizeof(int) * size);
+            clause_sizes[clause_index] = size;
+            clause_stamp[clause_index] = 0;
+
+            if (size == 2) {
+                add_bimp(-lits[0], lits[1]);
+                add_bimp(-lits[1], lits[0]);
+            }
+            clause_index++;


No bounds checking for clause_index. If the CNF file contains more clauses than MAX_CLAUSES (1000000), this will cause an array out-of-bounds access. Add a check to ensure clause_index < MAX_CLAUSES before accessing the arrays.

Copilot · 2026-02-18T06:49:48Z

+        propagated.push_back(var);
+
+        int idx = lit_index(l);
+        for (int i = 0; i < bimp_size[idx]; i++) global_queue[rear++] = bimp[idx][i];


No bounds checking for rear index in global_queue. If the number of propagated literals exceeds MAX_VARS + 1, this will cause an array out-of-bounds write. Add a check to prevent buffer overflow.

Copilot · 2026-02-18T06:49:48Z

+// ----------------- BCP ROUTINES -----------------
+// The following code is adapted from the provided BCP snippet.
+
+#define MAX_VARS 20000
+#define MAX_CLAUSES 1000000
+#define MAX_LITS 1000000
+#define BIMP_GROW_CHUNK 4
+#define ASSIGN_NONE 0
+#define ASSIGN_TRUE 1
+#define ASSIGN_FALSE 2
+
+int n_vars, n_clauses;
+int *clauses[MAX_CLAUSES];
+int clause_sizes[MAX_CLAUSES];
+int clause_stamp[MAX_CLAUSES];
+int *watch1[MAX_CLAUSES];
+int *watch2[MAX_CLAUSES];
+
+uint8_t assignments[MAX_VARS + 1];
+int current_stamp = 1;
+
+// Binary implication arrays
+int *bimp[MAX_VARS * 2 + 2];
+int bimp_size[MAX_VARS * 2 + 2];
+int bimp_capacity[MAX_VARS * 2 + 2];
+
+int var_activity[MAX_VARS + 1];
+int global_queue[MAX_VARS + 1];
+
+static inline int lit_index(int lit) {
+    return (lit > 0) ? lit : n_vars - lit;
+}
+
+static inline bool is_preselected(int var) {
+    return bimp_size[lit_index(var)] > 0 || bimp_size[lit_index(-var)] > 0;
+}
+
+static inline void reset_assignments() {
+    memset(assignments, ASSIGN_NONE, sizeof(uint8_t) * (n_vars + 1));
+    current_stamp++;
+}
+
+void add_bimp(int lit, int implied) {
+    int idx = lit_index(lit);
+    if (bimp_capacity[idx] == 0) {
+        bimp_capacity[idx] = BIMP_GROW_CHUNK;
+        bimp[idx] = (int*)malloc(sizeof(int) * bimp_capacity[idx]);
+    } else if (bimp_size[idx] >= bimp_capacity[idx]) {
+        bimp_capacity[idx] *= 2;
+        bimp[idx] = (int*)realloc(bimp[idx], sizeof(int) * bimp_capacity[idx]);
+    }
+    bimp[idx][bimp_size[idx]++] = implied;
+}
+
+void parse_cnf(const char *filename) {
+    FILE *fp = fopen(filename, "r");
+    if (!fp) {
+        perror("Error opening file");
+        exit(1);
+    }
+    char line[10000];
+
+    int clause_index = 0;
+    while (fgets(line, sizeof(line), fp)) {
+        if (line[0] == 'p') {
+            sscanf(line, "p cnf %d %d", &n_vars, &n_clauses);
+        } else if (line[0] != 'c') {
+            int lits[1000], size = 0, lit;
+            char *ptr = line;
+            while (sscanf(ptr, "%d", &lit) == 1 && lit != 0) {
+                lits[size++] = lit;
+                ptr = strchr(ptr, ' ');
+                if (!ptr) break;
+                ptr++;
+            }
+            clauses[clause_index] = (int *)malloc(sizeof(int) * size);
+            memcpy(clauses[clause_index], lits, sizeof(int) * size);
+            clause_sizes[clause_index] = size;
+            clause_stamp[clause_index] = 0;
+            if (size >= 2) {
+                watch1[clause_index] = &clauses[clause_index][0];
+                watch2[clause_index] = &clauses[clause_index][1];
+            }
+            if (size == 2) {
+                add_bimp(-lits[0], lits[1]);
+                add_bimp(-lits[1], lits[0]);
+            }
+            if (size <= 3) {
+                for (int j = 0; j < size; j++)
+                    var_activity[abs(lits[j])]++;
+            }
+            clause_index++;
+        }
+    }
+    n_clauses = clause_index;
+    fclose(fp);
+}


Significant code duplication detected. The BCP (Boolean Constraint Propagation) routines, CNF parsing logic, and related data structures are nearly identical between simple_mcts.cpp and beam_lookahead.cpp. Consider extracting this common functionality into a shared header file or library to improve maintainability and reduce duplication.

… preselection logic

…ting watch lists

Add per-depth normalization and risk-aware beam scoring

c6cc5b4

Copilot AI review requested due to automatic review settings February 18, 2026 06:43

piyush-J added the codex label Feb 18, 2026 — with ChatGPT Codex Connector

Copilot started reviewing on behalf of piyush-J February 18, 2026 06:44 View session

Add runtime timing stats to beam_lookahead output

5c71403

Copilot AI reviewed Feb 18, 2026

View reviewed changes

piyush-J and others added 4 commits February 18, 2026 12:19

Refresh README beam lookahead non-debug output example

19c0dcd

Improve variable selection by implementing unit variable tracking and…

f18624e

… preselection logic

Add lightweight mode for depth-1 scoring in main function

e3597ff

Refactor clause propagation by implementing watched literals and upda…

80a8b2b

…ting watch lists

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Codex-generated pull request#2

Codex-generated pull request#2
piyush-J wants to merge 6 commits into
mainfrom
codex/explain-alphamaplesat-algorithm-dh4561

piyush-J commented Feb 18, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Feb 18, 2026

Uh oh!

Copilot AI Feb 18, 2026

Uh oh!

Copilot AI Feb 18, 2026

Uh oh!

Copilot AI Feb 18, 2026

Uh oh!

Copilot AI Feb 18, 2026

Uh oh!

Copilot AI Feb 18, 2026

Uh oh!

Copilot AI Feb 18, 2026

Uh oh!

Copilot AI Feb 18, 2026

Uh oh!

Copilot AI Feb 18, 2026

Uh oh!

Copilot AI Feb 18, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

-            printf("        S2_mean=(%.3f+%.3f)/2=%.3f\n", s2_plus, s2_minus, s2_mean);
-            printf("        S2_balanced=%.3f - %.2f*|%.3f-%.3f| = %.3f\n",
-                   s2_mean, gamma, s2_plus, s2_minus, s2_balanced);
-        }
-    }
-    double max_s1 = 1e-9, max_s2 = 1e-9;
-    for (const auto& u : updated) {
-        max_s1 = max(max_s1, u.s1);
-        max_s2 = max(max_s2, u.s2_balanced);
-    }
-    for (auto& u : updated) {
-        u.s1_norm = u.s1 / max_s1;
+    double max_s1 = 0.0, max_s2 = 0.0;
+    for (const auto& u : updated) {
+        if (u.s1 > max_s1) {
+            max_s1 = u.s1;
+        }
+        if (u.s2_balanced > max_s2) {
+            max_s2 = u.s2_balanced;
+        }
+    }
+    const double norm_s1_den = (max_s1 > 0.0) ? max_s1 : 1.0;
+    const double norm_s2_den = (max_s2 > 0.0) ? max_s2 : 1.0;
+    for (auto& u : updated) {
+        u.s1_norm = (max_s1 > 0.0) ? (u.s1 / norm_s1_den) : 0.0;
+        u.s2_norm = (max_s2 > 0.0) ? (u.s2_balanced / norm_s2_den) : 0.0;
+        u.updated_score = (1.0 - lambda) * u.s1_norm + lambda * u.s2_norm;
+        if (debug) {
+            printf("\n[debug] normalize+combine for x=%d\n", u.seed_var);
+            printf("        S1_norm=%.3f/%.3f=%.6f\n", u.s1, norm_s1_den, u.s1_norm);
+            printf("        S2_norm=%.3f/%.3f=%.6f\n", u.s2_balanced, norm_s2_den, u.s2_norm);

		clauses[clause_index] = (int)malloc(sizeof(int) size);
		memcpy(clauses[clause_index], lits, sizeof(int) * size);

Conversation

piyush-J commented Feb 18, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Feb 18, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 18, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 18, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 18, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 18, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 18, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 18, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 18, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 18, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 18, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants