gpupsat2

CUDA SAT solver featuring:

• Two-watched-literals

• VSIDS

• 1-UIP learning

• Geometric restarts

• "Portfolio" or cube-and-conquer dispatch options

CPU port from the same sources in cpupsat/ runs 4–5× faster on the same hardware, proving that there is totally no point in solving SAT on GPUs.

(CDCL is the worst-case GPU workload. Per-thread pointer-chasing through watch lists with branchy conflict analysis means a warp has 32 threads taking 32 different control-flow paths, so the SM runs at ~1/32 utilization. And ~3× faster per-thread CPU clocks and L2/L3 caches actually work for the unpredictable watcher accesses.)

Build

GPU (CUDA 12.x):

cmake -B build -DCMAKE_BUILD_TYPE=Release -DCUDA_COMPUTE_CAPABILITY=89
cmake --build build --config Release -j16

CPU (C++20):

cmake -B cpupsat/build -S cpupsat -DCMAKE_BUILD_TYPE=Release
cmake --build cpupsat/build --config Release -j16

Run

build/Release/gpupsat2.exe        -i tests/factoring_7_4.cnf
cpupsat/build/Release/cpupsat.exe -i tests/factoring_7_4.cnf

DIMACS in, SATISFIABLE / UNSATISFIABLE / INDETERMINATE out.

CLI

Flag	Meaning
-i, --input <file>	DIMACS CNF (required)
-m, --mode portfolio|partition	dispatch (default portfolio)
--cube-vars K	partition only: 2^K cubes, 1 ≤ K ≤ 30
-t, --threads N	work-items / arena slices
-w, --workers N	concurrent OS threads (CPU only; default = hardware_concurrency())
-b, --blocks N	grid blocks (GPU only)
-c, --config <file>	TOML config (default ./config.toml)
-q, --quiet	suppress info & stats output

In portfolio mode, each work-item runs an independent CDCL search with its own RNG seed; first to terminate wins. In partition mode, 2^K cubes are distributed across -t arena slices via an atomic cursor; SAT in any cube wins, global UNSAT fires once every cube has been ruled out.

Runtime stats

Unless -q, every run prints a per-work-item stats block:

Solved in 0.82 ms (winner=work-item 0)
Stats (across 32 work-items):
  decisions                 total=30        min=0  max=18    mean=1
  conflicts                 total=0         min=0  max=0     mean=0
  propagations              total=53        min=0  max=32    mean=2
  restarts                  total=0         min=0  max=0     mean=0
  learned_added             total=0         min=0  max=0     mean=0
  learn_overflow_rejections total=0         ...               threads_with=0
  learned_evictions         total=0         ...               threads_with=0
  learned_flushes           total=0         ...               threads_with=0
  ns_propagate              total=9,900     min=0  max=5,500 mean=309
  ns_analyze                total=0         min=0  max=0     mean=0
  (propagate 0.0%, analyze 0.0% of wall*work-items)
Exit reasons: SAT=1 UNSAT=0 UNDEF=31

threads_with on the overflow/eviction/flush rows counts how many work-items hit that path — a thrash signal. The GPU build reports cycles_propagate / cycles_analyze (SM clock cycles) instead of nanoseconds.

config.toml

Optional, loaded from ./config.toml next to the binary unless -c overrides. Missing keys fall back to defaults; missing file is silently OK unless -c is explicit.

[restart]
initial_budget = 100      # conflicts before first restart
growth_factor  = 1.5      # geometric growth per restart

[twl]
vsids_mult         = 1e-30   # rescale factor when activity hits threshold
vsids_threshold    = 1e30
vsids_decay        = 0.95
glue_lbd_threshold = 2       # LBD ≤ this is "glue", retained on eviction

[cdcl]
max_learned_clauses = 65536  # per-thread cap (mlc)
max_learned_lits    = 0      # 0 = auto from mlc * avg_clause_len * ratio
mll_auto_ratio_num  = 3
mll_auto_ratio_den  = 2
mll_auto_min_avg    = 2
learned_pad_floor   = 4      # extra slack per learned-watcher bucket
max_conflicts       = 0      # 0 = unlimited; non-zero exits to UNDEF as escape hatch

[rng]
activity_init_min = 0.0      # range for per-thread random initial VSIDS scores
activity_init_max = 1e-6

max_conflicts is a debug option: set it non-zero on instances that don't terminate to get the stats block out instead of a hang.

---

P.S. Totally claude-coded, of course.