From e5df861d665080319a031e205e6f90a0e0def170 Mon Sep 17 00:00:00 2001
From: GothicTomato <106775154+GothicTomato@users.noreply.github.com>
Date: Sun, 17 Jul 2022 14:13:02 -0400
Subject: [PATCH] Create README.md

---
 README.md | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 README.md

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..b53421d
--- /dev/null
+++ b/README.md
@@ -0,0 +1,11 @@
+# psat
+
+Experimental SAT solver using OpenCL on GPU.
+
+Make sure that the work group size is set correctly for your GPU (in gpusolver.c). At some point I'll integrate auto-detection, but that day is not today.
+
+Plenty of optimizations left to be done, as well as algorithmic changes, particularly to the subsumption check routine.
+
+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).