Deployed a live demo of a SAT classification engine that can predict the satisfiability of hard instances without actually invoking a solver.
Right now, it successfully classifies 57% of hard instances with 99.9% accuracy (tested on SATLIB benchmarks), running 47x faster than MiniSAT on those specific cases.
You can try it out here: ptsf-engine.vercel.app
Access Token: FASTFAST (Valid for the next 6 hours- posted 4am PST 6/12)
How it works (and what's next)
The current live engine is purely a classifier. It analyzes the structural features of a standard DIMACS .cnf file to make high-confidence predictions before a heavy solver ever touches it.
However, the classifier is just phase one. I'm currently building the full solver:
The Core: A ground-up CDCL (Conflict-Driven Clause Learning) implementation written in Rust.
Current Status: The Python prototype already beats standard DPLL by 2x to 5x. The Rust implementation is being optimized to compete with state-of-the-art solvers like Kissat—projecting to be 3x to 4x faster on specific instance classes that matter most for hardware verification. Open to adding team members to bring to commercialization as high speed chip designers or sell to a behemoth.
Right now, it successfully classifies 57% of hard instances with 99.9% accuracy (tested on SATLIB benchmarks), running 47x faster than MiniSAT on those specific cases.
You can try it out here: ptsf-engine.vercel.app
Access Token: FASTFAST (Valid for the next 6 hours- posted 4am PST 6/12)
How it works (and what's next) The current live engine is purely a classifier. It analyzes the structural features of a standard DIMACS .cnf file to make high-confidence predictions before a heavy solver ever touches it.
However, the classifier is just phase one. I'm currently building the full solver:
The Core: A ground-up CDCL (Conflict-Driven Clause Learning) implementation written in Rust.
Current Status: The Python prototype already beats standard DPLL by 2x to 5x. The Rust implementation is being optimized to compete with state-of-the-art solvers like Kissat—projecting to be 3x to 4x faster on specific instance classes that matter most for hardware verification. Open to adding team members to bring to commercialization as high speed chip designers or sell to a behemoth.