LogicSpace Architecture

CNF in, CNF out

POST /cnf  {"dimacs": "p cnf 3 2\n1 2 3 0\n-1 -2 0"}

Returns commented DIMACS:

  SAT   → c solution: 5 forced variables
          v 1 -2 3 -4 5 0

  UNSAT → c empty clause derived from polynomial techniques
          0

  OPEN  → c simplified: 150 clauses, 400 lits
          c reduction: 1278L -> 400L (68.7%)
          1 2 0
          -3 4 0
          ...

Pipeline

  CNF input
      │
      ▼
  DualTree.compile(clauses, vocabulary)     O(n·m)
      │  BCP tree: log(n) depth, 2n nodes
      │  learned clauses from every branch
      │
      ▼
  Vivify original against enriched BCP       O(m·k)
      │  assume negation of original clause lits
      │  on enriched solver → contradiction = drop lit
      │
      ▼
  PolySAT tier 0-5                           O(n²) to O(n²m)
      │  BCP → 2-SAT → XOR → Gauss → BCE
      │  → subsume → BVE → vivify → probe
      │
      ▼
  simplified_cnf()
      │  ≤ original, every clause is a subset
      │  sorted by width (short first)
      │
      ├── SAT?    → solution from forced lits
      ├── UNSAT?  → empty clause
      └── OPEN?   → pass to next worker

Lambda Architecture

  Orchestrator  (512MB, 300s)
      │
      │  1. Compute vocabulary (achilles, once)
      │  2. Fire worker tree
      │  3. Collect learned clauses
      │  4. Vivify original at root
      │  5. If shrunk → loop. Else → fixpoint.
      │
      ▼
  Worker  (2.3GB, 300s, self-recursive)
      │
      ├── DualTree.compile(simplified, vocab)
      ├── Branch on vocab[depth]: +v, -v
      ├── Fire two child Lambdas concurrently
      ├── as_completed: first result enriches parent
      └── Return learned clauses uphill

  Workers explore. Root simplifies.
  shrunk = true  → formula got smaller → recurse
  shrunk = false → polynomial fixpoint → stop

  Depth log(n) = n leaf workers = polynomial total cost.

Proven Results

Charles Dana • Tulane University • Monce SAS • April 2026