From c7a2f3f95a5af31010e058fbc168a2aab628a72a Mon Sep 17 00:00:00 2001 From: gothictomato Date: Sun, 17 Jul 2022 19:23:53 -0400 Subject: [PATCH] Fixed CMakeLists.txt --- CMakeLists.txt | 2 +- README.md | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index d0d9663..1f71281 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -4,6 +4,6 @@ project(psat C) set(CMAKE_C_STANDARD 99) set(CMAKE_C_FLAGS "-O3") -add_executable(psat main.c cnf.c cnf.h time.c time.h types.h gpusolver.c gpusolver.h sstree.c sstree.h cpusolver.c cpusolver.h) +add_executable(psat main.c cnf.c cnf.h time.c time.h types.h gpusolver.c gpusolver.h cpusolver.c cpusolver.h) target_link_libraries(psat -lOpenCL) \ No newline at end of file diff --git a/README.md b/README.md index b53421d..c2b5178 100644 --- a/README.md +++ b/README.md @@ -9,3 +9,5 @@ Plenty of optimizations left to be done, as well as algorithmic changes, particu For now the algorithm only operates on a single local workgroup, but it'll be expanded to maintain and run on several independent counters. After that, I plan on integrating work re-balancing: periodically, the work groups will sync with eachother, and in case of a work group having proven its range unsat, the next largest work group will be split between the two. The CPU-bound version of this algorithm is currently about 2x as fast, when I set the local workgroup size to 256. However, the CPU-bound version also takes advantage of early exit scenarios that this algorithm can, but doesn't take advantage of (yet). + +I'm currently not sure what the best approach is, optimization-wise, out of the ideas I currently have, \ No newline at end of file