diff --git a/CFLOBDD/tests_cfl.cpp b/CFLOBDD/tests_cfl.cpp index 57f56aa..a8c0677 100644 --- a/CFLOBDD/tests_cfl.cpp +++ b/CFLOBDD/tests_cfl.cpp @@ -1949,6 +1949,115 @@ 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 row */ + for (l = 0; l < n; l++) { + if (l != j) { + CFLOBDD mp = MkImplies(vars[i][j], MkNot(vars[i][l])); + a = MkAnd(a, mp); + } + } + + /* 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])); + b = MkAnd(b, mp); + } + } + + /* No one in the same up-right diagonal */ + for (k = 0; k < n; k++) { + 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])); + c = MkAnd(c, mp); + } + } + } + + /* No one in the same down-right diagonal */ + for (k = 0; k < n; 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])); + 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; + 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){ CFLTests::InitModules(); @@ -2214,6 +2323,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..8016b27 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 @@ -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" @@ -52,7 +56,12 @@ 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_link_libraries(cflobdd_test m) -target_compile_definitions(cflobdd_test PUBLIC PATH_COUNTING_ENABLED) +# target_compile_definitions(cflobdd_test PUBLIC PATH_COUNTING_ENABLED) + +if(WCFLOBDD_SUPPORTED) + target_compile_definitions(cflobdd PUBLIC WCFLOBDD_SUPPORTED) + target_compile_definitions(cflobdd_test PUBLIC WCFLOBDD_SUPPORTED) +endif()