Technical architecture
An end-to-end reasoning pipeline. Each stage is independently testable, instrumented, and replaceable — a real systems product, not a monolithic solver wrapper.
LaTeX, natural language, raw text, or DIMACS — accepted as-is. No format gate.
Gemini-3-Flash via Lovable AI Gateway translates messy input into strict DIMACS only when the deterministic parser fails.
Tseitin encoding of propositional formulas with structural variable tracking and short-circuit primitives.
Header reconciliation, literal compaction, redundant-clause elimination, variable elimination, pure-literal lifts.
Structure-aware branching combining VSIDS, LBD, and learning-rate signals; AI-assisted variable ordering as a configurable layer.
First-UIP conflict analysis, glue-based clause retention, restart policy tuned per workload family.
Threadripper-class portfolio with clause-sharing, diversified seeds, and bounded memory-per-worker.
DRAT-trim certified UNSAT proofs and explicit SAT witness emission. Every result is auditable.
Data path
user input ── LaTeX | text | DIMACS
│
▼
[parseDimacs] ────────────┐ on failure
│ ok ▼
│ [llmNormalizeToDimacs] (Gemini-3-Flash)
│ │
▼ ▼
┌────────── canonical CNF (Tseitin) ──────────┐
│ │
▼ ▼
[preprocessor] [proof recorder]
│ unit propagation │
│ VE / pure literals │
▼ │
[solver portfolio] ── Threadripper · 96C/192T │
│ CDCL · VSIDS · LBD · restarts │
▼ │
{SAT model} | {UNSAT cert} ───── DRAT-trim ◄─┘
│ │
└──── verify ◄───┘