kauai1
27 karma · joined March 27, 2026
PTSF (Parks Tensorial SAT Framework) — Rust · deployed · ptsf-engine.vercel.app
SAT classification engine that resolves a large share of instances before search begins. Returns UNSAT on Schur_161_5_d38 in 580ms — an instance Kissat 4.0.4 leaves unanswered at 120s and CaDiCaL at 300s — with ground truth from a published theorem. Answers 11 SC2024 instances Kissat can’t resolve in 10s; 7.5× geometric-mean speedup over Kissat on random 3-SAT at n=75–100. Error rate published alongside: 50 commitments on the labelled SC2024 set, 39 correct. Verdicts are labelled proved or heuristic so nothing reads as certain unless it’s checkable. Still improving the engine.