PTSF · SAT Classification Engine
Physics, Fast
& More Capable.
PTSF classifies SAT instances using proprietary structural signals extracted from the constraint structure itself. No search. No resolution. No CDCL.
On instances the world's best solvers cannot answer at all, PTSF answers in milliseconds.
86.6%
SC2023 industrial instances
classified without solver
117ms
median classification time
SC2023 main track
SATLIB
Validated range
n=15 to n=500 validated
0
false classifications
on verified instances
Regime declaration
Kissat — three-time SAT Competition gold medalist — times out on the majority of these instances. PTSF does not compete on Kissat's terms. It operates on a different physical principle: proprietary structural inference rather than resolution-based search. This inference takes milliseconds. The proof would take exponential time.
Head to head
PTSF vs State of the Art
Pigeonhole n=800
rphp_p20_r20 · SC2023
TIMEOUT
UNSAT · 51ms
Hardware verification n=176–526
BZ2File, php15–18 · SC2023
TIMEOUT
UNSAT · 20–80ms
Schur numbers n=755–756
SC2023 main track
TIMEOUT
UNSAT · 41ms
Argumentation / SCPC n=700–1000
SC2023 main track
TIMEOUT
UNSAT · 25–170ms
Random 3-SAT n=20–100
Rust VIG-CDCL solver
baseline
3.9× faster mean
9.7× peak at n=75
Random 3-SAT n=15–500
Tier 1 classifier
solves (slower)
majority resolved without solver · <10ms
high accuracy
PTSF's advantage on industrial instances is both a speed improvement and a capability boundary. On instances Kissat can solve, PTSF is 3.9× faster on average, 9.7× at peak. On instances Kissat cannot answer at all — timing out regardless of how long you wait — PTSF answers in milliseconds using proprietary signal inference rather than search. This is not a faster solver. This is a different class. And it was built, validated, and deployed on consumer hardware — the performance ceiling has not been found.
Architecture
↓ structured continue · random large → solver
Tier 1a
10–300ms · majority coverage
↓ ambiguous continue
Tier 1b
100–500ms · further coverage
↓ hard cases → solver
Tier 2
3.9× Kissat · 13.4% of instances
Validated performance
Numbers that impact
86.6%
Industrial classification rateSC2023 main track · n≤2000 · 119 instances
0
False classificationszero misclassifications on all verified instances
SATLIB
Validated rangen=15 to n=500
117ms
Median classification timeSC2023 industrial instances · no solver invoked
9.7×
Peak solver speedup vs KissatRust VIG-CDCL · n=75 · 100% correct
Majority
Solver call reductionrandom k-SAT · Tier 1 classifier · <10ms
High
Tier 1 accuracyrandom 3-SAT · SATLIB n=50–100 · 1000+ instances
3.9×
Mean solver speedup vs KissatRust VIG-CDCL · n=20–100 · validated
Live engine
Submit an instance
▲
drop .cnf file here or click to browse
or
| n | Result | Tier | ms |
|---|---|---|---|
| no classifications yet | |||
On 86.6% of real industrial SAT instances, PTSF's classifier returns a confirmed answer in a median of 117 milliseconds — on the exact instances where Kissat, the field's three-time gold-medal solver, does not return an answer at all within any practical time budget. This is not a speed comparison; it's a capability boundary.
On the remaining 13.4%, where a solver is genuinely required, PTSF routes to a purpose-built Rust solver that exceeds Kissat by the standard metric: 3.9× faster on average, 9.7× at peak.
This is a complete, robust pipeline — not a narrow optimization, but a system that outperforms the industry's best solver at both ends of the problem: where Kissat fails outright, and where it succeeds.
Work is actively underway expanding classification coverage to additional industrial instance families beyond the original benchmark set. One such case has returned an output independently confirmed against CaDiCaL — with PTSF returning the answer roughly 257× faster. A second has returned an output on an instance CaDiCaL could not answer at all within any practical time budget, and for which no independent secondary verification currently exists. If independently confirmed, these additional capabilities would extend the framework's total classification coverage toward 90%.