What it is

SATori is a conflict-driven clause-learning solver that fits in a single source file and compiles with no external libraries — from an x86 workstation down to a small embedded board, unchanged. It is not built to win competitions; it is built to be the most reliable solver in the tiny class on its target domain, while staying small enough to deploy where the heavyweight solvers cannot comfortably go.

Its headline component is a clause-span branching heuristic that orders decisions by each variable's structural reach across the clause sequence — favouring the "bridge" variables that connect distant parts of a planning formula. Every UNSAT verdict can be emitted as a DRAT proof and checked independently with drat-trim.

One file, zero dependencies. ~2,000 lines of C++; builds with a stock compiler.
Planning-aware. SCC substitution, failed-literal probing, temporal-band detection, and clause-span branching exploit the 85–99% binary-clause structure of planning CNFs.
Auditable. DRAT proofs for every UNSAT result — all certified in the corpus, no failures.
Embeddable. Peak 41 MB on a 427 MB armv6l board; memory scales sublinearly with instance size.

Performance

Evaluated under PAR-2 (timeouts charged at 2× the 100 s budget) against two tiny baselines and two state-of-the-art references. Lower PAR-2 is better.

x86_64 — 112 instances

Solver	PAR-2	geo. (nt)	Timeouts
SATori	5,886	465	2
MiniSat	11,307	373	6
PicoSAT	10,441	579	5

Kissat (SOTA)	6,471	341	3
CaDiCaL (SOTA)	4,985	447	2

Best PAR-2 of any tiny solver — ahead of Kissat — with only the far larger CaDiCaL lower. Its two timeouts are a strict subset of Kissat's; it never fails alone.

armv6l embedded — 36 instances

Solver	Solved	geo. (ms)	PAR-2
SATori	35 / 36	514	7,935
PicoSAT	35 / 36	501	9,839
MiniSat	32 / 36	4,324	31,184

On the embedded target SATori is the most reliable tiny solver — roughly 8× faster than MiniSat in geometric mean, and it solves large planning instances on which MiniSat times out.

Download & build

The solver is a single source file, satori-50.cpp, which compiles to the satori binary.

Download satori-50.cpp

1 — x86_64 build (performance)

$ g++ -O2 -fno-exceptions -fno-rtti -DNDEBUG satori-50.cpp -o satori

2 — Self-contained static binary (deployment)

$ g++ -O2 -fno-exceptions -fno-rtti -DNDEBUG -static -s satori-50.cpp -o satori

3 — armv6l / embedded (native on Alpine, musl)

# stock toolchain, no cross-compilation, no patches $ g++ -O2 satori-50.cpp -o satori

Run

$ ./satori problem.cnf # emit a DRAT proof for an UNSAT verdict and check it $ ./satori --proof proof.drat problem.cnf $ drat-trim problem.cnf proof.drat

-O3 and -march=native give no benefit over -O2 within the noise floor. -Os trades 25–45% of solving speed for a 38% smaller binary. The benchmarks used the dynamic build; -static -s is for deployment.