From a021752e4777ecf114ccf57bfa79dd46b4828d94 Mon Sep 17 00:00:00 2001 From: Zhenrong Gu Date: Wed, 15 Apr 2026 17:50:59 +0800 Subject: [PATCH 1/2] Add NQueens test, Fix CMake building script --- CFLOBDD/tests_cfl.cpp | 116 ++++++++++++++++++++++++++++++++++++++++++ CFLOBDD/tests_cfl.h | 1 + CMakeLists.txt | 10 ++-- 3 files changed, 123 insertions(+), 4 deletions(-) diff --git a/CFLOBDD/tests_cfl.cpp b/CFLOBDD/tests_cfl.cpp index 57f56aa..8deccd4 100644 --- a/CFLOBDD/tests_cfl.cpp +++ b/CFLOBDD/tests_cfl.cpp @@ -1949,6 +1949,120 @@ void CFLTests::ClearModules() #endif } +void CFLTests::testNQueens(int n) { + std::cout << "Testing " << n << "-Queens" << std::endl; + + auto start = high_resolution_clock::now(); + std::vector> vars; + unsigned int numVars = n * n; + unsigned int level = std::ceil(std::log2(numVars)); + for (unsigned int i = 0; i < n; i++) { + vars.push_back(std::vector()); + for (unsigned int j = 0; j < n; j++) { + vars[i].push_back(MkProjection(i * n + j, level)); + } + } + + std::vector orBatch; + for (unsigned int i = 0; i < n; i++) { + CFLOBDD condition = MkFalse(level); + for (unsigned int j = 0; j < n; j++) { + condition = MkOr(condition, vars[i][j]); + } + orBatch.push_back(condition); + } + + std::vector> impBatch; + + for (unsigned int i = 0; i < n; i++) { + std::cout << "Processing implications for row " << i << " / " << n << std::endl; + std::vector row; + for (unsigned int j = 0; j < n; j++) { + CFLOBDD a = MkTrue(level); + CFLOBDD b = MkTrue(level); + CFLOBDD c = MkTrue(level); + CFLOBDD d = MkTrue(level); + + unsigned int k, l; + + /* No one in the same column */ + for (l = 0; l < n; l++) { + if (l != j) { + printf("i = %d, j = %d, l = %d\n", i, j, l); + CFLOBDD mp = MkImplies(vars[i][j], MkNot(vars[i][l])); + a = MkAnd(a, mp); + } + } + + /* No one in the same row */ + for (k = 0; k < n; k++) { + if (k != i) { + CFLOBDD mp = MkImplies(vars[i][j], MkNot(vars[k][j])); + b = MkAnd(b, mp); + } + } + + /* No one in the same up-right diagonal */ + for (k = 0; k < n; k++) { + unsigned int ll = k - i + j; + if (ll >= 0 && ll < n) { + if (k != i) { + CFLOBDD mp = MkImplies(vars[i][j], MkNot(vars[k][ll])); + c = MkAnd(c, mp); + } + } + } + + /* No one in the same down-right diagonal */ + for (k = 0; k < n; k++) { + unsigned int ll = i + j - k; + if (ll >= 0 && ll < n) { + if (k != i) { + CFLOBDD mp = MkImplies(vars[i][j], MkNot(vars[k][ll])); + d = MkAnd(d, mp); + } + } + } + + c = MkAnd(c, d); + b = MkAnd(b, c); + a = MkAnd(a, b); + row.push_back(a); + } + impBatch.push_back(row); + } + + CFLOBDD queen = MkTrue(level); + + for (unsigned int i = 0; i < n; i++) { + std::cout << "Combining OR conditions for row " << i << " / " << n << std::endl; + queen = MkAnd(queen, orBatch[i]); + } + + for (unsigned int i = 0; i < n; i++) { + CFLOBDD tmp_queen = MkTrue(level); + for (unsigned int j = 0; j < n; j++) { + std::cout << "Combining implication conditions for position (" << i << ", " << j << ") " << " / " << n << std::endl; + tmp_queen = MkAnd(tmp_queen, impBatch[i][j]); + } + queen = MkAnd(queen, tmp_queen); + } + + auto end = high_resolution_clock::now(); + auto duration = duration_cast(end - start); + std::cout << "Duration: " << duration.count() << " ms" << std::endl; + // unsigned int numDummyVars = std::pow(2, std::ceil(std::log2(numVars))) - numVars; + // std::cout << "Number of dummy variables: " << numDummyVars << " " << std::pow(2, std::ceil(std::log2(numVars))) << " " << numVars << std::endl; + // queen.CountPaths(); + // unsigned int nodeCount = 0, edgeCount = 0; + // queen.CountNodesAndEdges(nodeCount, edgeCount); + // std::cout << "nodeCount: " << nodeCount << " edgeCount: " << edgeCount << " totalCount: " << (nodeCount + edgeCount) << std::endl; + // CFLOBDDInternalNode* queen_node = (CFLOBDDInternalNode*) queen.root->rootConnection.entryPointHandle->handleContents; + // // std::cout << "Number of non-solutions for " << n << "-Queens: " << queen_node->numPathsToExit[0] << std::endl; + // std::cout << "Number of solutions for " << n << "-Queens: " << queen_node->numPathsToExit[1] / std::pow(2, numDummyVars) << std::endl; + // std::cout << "Number of solutions for " << n << "-Queens: " << queen_node->numPathsToExit[1] << std::endl; +} + bool CFLTests::runTests(const char *arg, int size, int seed, int a){ CFLTests::InitModules(); @@ -2214,6 +2328,8 @@ bool CFLTests::runTests(const char *arg, int size, int seed, int a){ // Test VerifySubtractiveKaratsubaOneLevelModuliwise std::cout << "Testing VerifySubtractiveKaratsubaOneLevelModuliwise" << std::endl; VerifySubtractiveKaratsubaOneLevelModuliwise(); + } else if (curTest == "nqueens") { + CFLTests::testNQueens(size); } else { std::cout << "Unrecognized test name: " << curTest << std::endl; diff --git a/CFLOBDD/tests_cfl.h b/CFLOBDD/tests_cfl.h index 87f6824..9fbf30f 100644 --- a/CFLOBDD/tests_cfl.h +++ b/CFLOBDD/tests_cfl.h @@ -54,6 +54,7 @@ class CFLTests static void testXOR(int size); static void testMatMul(int size); static void testQFT(int size, int seed); + static void testNQueens(int size); #ifdef WCFLOBDD_SUPPORTED static void testWeightedOps(unsigned int size); diff --git a/CMakeLists.txt b/CMakeLists.txt index 38943c7..ed808e6 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,8 +1,8 @@ cmake_minimum_required(VERSION 3.12) project(cflobdd) -# Set the C++ standard to 17, as specified in the compile command -set(CMAKE_CXX_STANDARD 17) +# Set the C++ standard to 20, as specified in the compile command +set(CMAKE_CXX_STANDARD 20) set(CMAKE_CXX_STANDARD_REQUIRED ON) # Add compiler flags: -g for debugging and -w to suppress warnings @@ -52,7 +52,9 @@ add_custom_target(cflobdd_java ALL DEPENDS ${CFLOBDD_DIR}/java_bindings/target/c # Link the math library. target_link_libraries(cflobdd m) -target_compile_definitions(cflobdd PUBLIC PATH_COUNTING_ENABLED) +# target_compile_definitions(cflobdd PUBLIC PATH_COUNTING_ENABLED) +target_compile_definitions(cflobdd PUBLIC WCFLOBDD_SUPPORTED) target_link_libraries(cflobdd_test m) -target_compile_definitions(cflobdd_test PUBLIC PATH_COUNTING_ENABLED) +# target_compile_definitions(cflobdd_test PUBLIC PATH_COUNTING_ENABLED) +target_compile_definitions(cflobdd_test PUBLIC WCFLOBDD_SUPPORTED) From d3dd3c6b66135483c828db1c6322e85ea79fe746 Mon Sep 17 00:00:00 2001 From: Zhenrong Gu Date: Thu, 16 Apr 2026 12:30:52 +0800 Subject: [PATCH 2/2] fix(tests_cfl): fix the unsigned integer underflow bug; output the number of solutions for NQueens fix(CMakeLists): conditionally include weighted sources and definitions --- CFLOBDD/tests_cfl.cpp | 49 +++++++++++++++++++------------------------ CMakeLists.txt | 13 +++++++++--- 2 files changed, 32 insertions(+), 30 deletions(-) diff --git a/CFLOBDD/tests_cfl.cpp b/CFLOBDD/tests_cfl.cpp index 8deccd4..a8c0677 100644 --- a/CFLOBDD/tests_cfl.cpp +++ b/CFLOBDD/tests_cfl.cpp @@ -1950,9 +1950,9 @@ void CFLTests::ClearModules() } void CFLTests::testNQueens(int n) { - std::cout << "Testing " << n << "-Queens" << std::endl; + std::cout << "Testing " << n << "-Queens" << std::endl; - auto start = high_resolution_clock::now(); + auto start = high_resolution_clock::now(); std::vector> vars; unsigned int numVars = n * n; unsigned int level = std::ceil(std::log2(numVars)); @@ -1975,26 +1975,25 @@ void CFLTests::testNQueens(int n) { std::vector> impBatch; for (unsigned int i = 0; i < n; i++) { - std::cout << "Processing implications for row " << i << " / " << n << std::endl; - std::vector row; + std::cout << "Processing implications for row " << i << " / " << n << std::endl; + std::vector row; for (unsigned int j = 0; j < n; j++) { CFLOBDD a = MkTrue(level); - CFLOBDD b = MkTrue(level); - CFLOBDD c = MkTrue(level); - CFLOBDD d = MkTrue(level); + CFLOBDD b = MkTrue(level); + CFLOBDD c = MkTrue(level); + CFLOBDD d = MkTrue(level); unsigned int k, l; - /* No one in the same column */ + /* No one in the same row */ for (l = 0; l < n; l++) { if (l != j) { - printf("i = %d, j = %d, l = %d\n", i, j, l); CFLOBDD mp = MkImplies(vars[i][j], MkNot(vars[i][l])); a = MkAnd(a, mp); } } - /* No one in the same row */ + /* No one in the same column */ for (k = 0; k < n; k++) { if (k != i) { CFLOBDD mp = MkImplies(vars[i][j], MkNot(vars[k][j])); @@ -2004,7 +2003,7 @@ void CFLTests::testNQueens(int n) { /* No one in the same up-right diagonal */ for (k = 0; k < n; k++) { - unsigned int ll = k - i + j; + int ll = (int)k - (int)i + (int)j; if (ll >= 0 && ll < n) { if (k != i) { CFLOBDD mp = MkImplies(vars[i][j], MkNot(vars[k][ll])); @@ -2015,7 +2014,7 @@ void CFLTests::testNQueens(int n) { /* No one in the same down-right diagonal */ for (k = 0; k < n; k++) { - unsigned int ll = i + j - k; + int ll = (int)i + (int)j - (int)k; if (ll >= 0 && ll < n) { if (k != i) { CFLOBDD mp = MkImplies(vars[i][j], MkNot(vars[k][ll])); @@ -2029,38 +2028,34 @@ void CFLTests::testNQueens(int n) { a = MkAnd(a, b); row.push_back(a); } - impBatch.push_back(row); + impBatch.push_back(row); } CFLOBDD queen = MkTrue(level); for (unsigned int i = 0; i < n; i++) { - std::cout << "Combining OR conditions for row " << i << " / " << n << std::endl; + std::cout << "Combining OR conditions for row " << i << " / " << n << std::endl; queen = MkAnd(queen, orBatch[i]); } for (unsigned int i = 0; i < n; i++) { - CFLOBDD tmp_queen = MkTrue(level); + CFLOBDD tmp_queen = MkTrue(level); for (unsigned int j = 0; j < n; j++) { - std::cout << "Combining implication conditions for position (" << i << ", " << j << ") " << " / " << n << std::endl; + std::cout << "Combining implication conditions for position (" << i << ", " << j << ") " << " / " << n << std::endl; tmp_queen = MkAnd(tmp_queen, impBatch[i][j]); } - queen = MkAnd(queen, tmp_queen); + queen = MkAnd(queen, tmp_queen); } auto end = high_resolution_clock::now(); auto duration = duration_cast(end - start); std::cout << "Duration: " << duration.count() << " ms" << std::endl; - // unsigned int numDummyVars = std::pow(2, std::ceil(std::log2(numVars))) - numVars; - // std::cout << "Number of dummy variables: " << numDummyVars << " " << std::pow(2, std::ceil(std::log2(numVars))) << " " << numVars << std::endl; - // queen.CountPaths(); - // unsigned int nodeCount = 0, edgeCount = 0; - // queen.CountNodesAndEdges(nodeCount, edgeCount); - // std::cout << "nodeCount: " << nodeCount << " edgeCount: " << edgeCount << " totalCount: " << (nodeCount + edgeCount) << std::endl; - // CFLOBDDInternalNode* queen_node = (CFLOBDDInternalNode*) queen.root->rootConnection.entryPointHandle->handleContents; - // // std::cout << "Number of non-solutions for " << n << "-Queens: " << queen_node->numPathsToExit[0] << std::endl; - // std::cout << "Number of solutions for " << n << "-Queens: " << queen_node->numPathsToExit[1] / std::pow(2, numDummyVars) << std::endl; - // std::cout << "Number of solutions for " << n << "-Queens: " << queen_node->numPathsToExit[1] << std::endl; + queen.CountPaths(); + CFLOBDDInternalNode* queen_node = (CFLOBDDInternalNode*) queen.root->rootConnection.entryPointHandle.handleContents; + + // number of solutions = 2 ^ log(num_solutions) / 2 ^ num_dummy_vars = 2^(log(num_solutions) - num_dummy_vars) + unsigned int numDummyVars = std::pow(2, std::ceil(std::log2(numVars))) - numVars; + std::cout << "Number of solutions for " << n << "-Queens: " << std::round(std::pow(2, queen_node->numPathsToExit[1] - numDummyVars)) << std::endl; } bool CFLTests::runTests(const char *arg, int size, int seed, int a){ diff --git a/CMakeLists.txt b/CMakeLists.txt index ed808e6..8016b27 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -28,10 +28,14 @@ file(GLOB SOURCES "${CFLOBDD_DIR}/*.cpp" "${CFLOBDD_DIR}/Solver/uwr/bit_vector/*.cpp" "${CFLOBDD_DIR}/Solver/uwr/parsing/*.cpp" - "${CFLOBDD_DIR}/cflobdd_c.cpp" ) list(REMOVE_ITEM SOURCES "${CFLOBDD_DIR}/main.cpp") +if(NOT WCFLOBDD_SUPPORTED) + file(GLOB WEIGHTED_SOURCES "${CFLOBDD_DIR}/weighted_*.cpp" "${CFLOBDD_DIR}/w*.cpp") + list(REMOVE_ITEM SOURCES ${WEIGHTED_SOURCES}) +endif() + file(GLOB JAVA_SOURCES "${CFLOBDD_DIR}/java_bindings/src/main/java/org/trishullab/cflobdd/*.java" "${CFLOBDD_DIR}/java_bindings/src/main/java/org/trishullab/cflobdd/api/jdd/*.java" @@ -53,8 +57,11 @@ add_custom_target(cflobdd_java ALL DEPENDS ${CFLOBDD_DIR}/java_bindings/target/c # Link the math library. target_link_libraries(cflobdd m) # target_compile_definitions(cflobdd PUBLIC PATH_COUNTING_ENABLED) -target_compile_definitions(cflobdd PUBLIC WCFLOBDD_SUPPORTED) target_link_libraries(cflobdd_test m) # target_compile_definitions(cflobdd_test PUBLIC PATH_COUNTING_ENABLED) -target_compile_definitions(cflobdd_test PUBLIC WCFLOBDD_SUPPORTED) + +if(WCFLOBDD_SUPPORTED) + target_compile_definitions(cflobdd PUBLIC WCFLOBDD_SUPPORTED) + target_compile_definitions(cflobdd_test PUBLIC WCFLOBDD_SUPPORTED) +endif()