Hardware
AMD Threadripper PRO 7995WX · 96C/192T · 512 GB ECC
Baselines
5 solvers, SAT Race 2024 builds
Instance suites
SATLIB, SAT Competition Main + Crafted
Proof checking
DRAT-trim certified UNSAT proofs
Solver matrix
Reference solvers used as baselines.
v0.3 · 2026-Q2 protocol
| Solver | Family | Build | Status |
|---|---|---|---|
| Kissat | SAT Race 2024 reference baseline | SAT-Race-2024 | PASS · integrated |
| CaDiCaL | Industrial workhorse, CDCL | SAT-Race-2024 | PASS · integrated |
| CryptoMiniSat | Crypto / XOR-aware reasoning | SAT-Race-2024 | PASS · integrated |
| Glucose | LBD-based clause management | SAT-Race-2024 | PASS · integrated |
| MapleSAT | Learning-rate branching | SAT-Race-2024 | PASS · integrated |
Methodology
Timeout policy
5,000 s wall-clock per instance, single-thread, identical CPU pinning and RSS cap across all solvers.
Instance selection
SATLIB uniform-random k-SAT, SAT Competition 2023–2024 Main and Crafted tracks, plus internal verification workloads.
Scoring
PAR-2 score on solved instances, with separate SAT/UNSAT breakdowns and per-family wall-clock distributions.
Reproducibility
Container images, seeds, raw runlogs, and DRAT proofs published per release.
Headline results — preview
Results below reflect KARIOS v0.3 against SAT Race 2024 baselines on selected DIMACS classes. Full per-instance tables and DRAT proofs are released with each tagged version.
| Suite | Instances | Solved (baseline) | Solved (KARIOS) | PAR-2 Δ |
|---|---|---|---|---|
| Hardware verification (industrial) | 184 | 121 | — | in progress |
| Crypto (CMS-aware) | 96 | 47 | — | in progress |
| Crafted / combinatorial | 132 | 68 | — | in progress |
| Uniform-random 3-SAT | 250 | 213 | — | in progress |
No fabricated numbers. Cells marked "—" will be populated with each release of the reproducibility package.