Dictionary-based SAT knowledge compiler. Submit a CNF, watch the dictionary learn.
Click any problem to open the resolution dashboard.
| Problem | Vars | Clauses | Entries | BB | Status |
|---|---|---|---|---|---|
| Pigeonhole 5->4 (UNSAT) | 20 | 45 | 40 | 0 | UNKNOWN |
| Random 3-SAT (100 vars, phase transition) | 100 | 426 | 1313 | 0 | UNKNOWN |
| unnamed | 20 | 85 | 258 | 0 | UNKNOWN |
| unnamed | 30 | 81 | 590 | 26 | UNSAT |
| unnamed | 75 | 319 | 918 | 0 | UNKNOWN |
| unnamed | 64 | 736 | 128 | 0 | UNKNOWN |
| unnamed | 50 | 213 | 603 | 0 | UNKNOWN |
| Implication chain x1->x2->...->x8->x1 | 8 | 8 | 16 | 0 | SAT |
| Petersen graph 3-coloring | 30 | 85 | 60 | 0 | UNKNOWN |
| Random 3-SAT (50 vars, ratio 4.26) | 50 | 213 | 634 | 0 | UNKNOWN |
| unnamed | 200 | 852 | 2515 | 0 | UNKNOWN |
| Mining 16b/4r difficulty=4 | 123 | 378 | 1045 | 4 | UNKNOWN |
| unnamed | 45 | 150 | 90 | 0 | UNKNOWN |
| Factor 15 = ? x ? (4-bit) | 163 | 485 | 1000 | 146 | UNKNOWN |
| unnamed | 50 | 217 | 716 | 41 | UNKNOWN |
| unnamed | 100 | 426 | 1232 | 0 | UNKNOWN |
| unnamed | 150 | 639 | 1879 | 0 | UNKNOWN |
POST /instances/clauses with {"n_vars": N, "clauses": [[1,-2,3], ...]}
POST /instances/dimacs with {"dimacs": "p cnf 3 2\n1 2 0\n-1 3 0\n"}
/instances/{id}/kpis •
/instances/{id}/solve •
/instances/{id}/deduce •
/instances/{id}/entries •
/instances/{id}/entry/detail •
/instances/{id}/entry/prune •
/instances/{id}/entry/extend_right •
/instances/{id}/prove •
/instances/{id}/extend •
/instances/{id}/achilles •
/instances/{id}/near-misses •
/instances/{id}/export/original •
/instances/{id}/export/reduced •
/instances/{id}/reduce •
/ui/{id}
Charles Dana • Tulane University • Monce SAS • April 2026