System 2: Strategic Reasoner (OB-SAT)
- Proposes decompositions (assumptions/cubes)
- Maintains an evolving strategic model:
- Region difficulty map
- Tensor edge hardness scores
- Structural conflict database (clause-level no-goods at S2 abstraction)
- Learns from S1's explanations to refine future proposals
System 1: Tactical Verifier (CDCL)
- Verifies S2's proposals under assumptions
- Explains failures richly:
- UNSAT cores (which assumptions caused conflict)
- Short learned clauses (LBD ≤ threshold)
- Performance signals (conflicts, LBD distribution, propagation rate)
- Does NOT emit cubes (that's S2's job)
New Interaction Architecture
┌─────────────────────────────────────────────────────────────┐
│ Problem Instance │
└─────────────────────────────────────────────────────────────┘
│
▼
┌─────────────────────────────────────────────────────────────┐
│ Initialize System 2 Internal State │
│ • Region difficulty map: Uniform(1.0) │
│ • Tensor edge hardness: Degree-based │
│ • Structural conflict DB: ∅ │
│ • Variable selection bias: Initial heuristic │
└─────────────────────────────────────────────────────────────┘
│
▼
┌────────────────────────────┐
│ Strategic Loop (S2) │
└────────────────────────────┘
│
┌──────────────────┴──────────────────┐
▼ ▼
┌─────────────────┐ ┌─────────────────┐
│ Gamma-1 Phase │ │ Branching Phase │
│ (Forced assign) │ │ (Strategic) │
└─────────────────┘ └─────────────────┘
│ │
│ Apply directly │
▼ ▼
┌─────────────────────────────────────────────────────────────┐
│ S2 Proposes Cube (Assumptions) │
│ • Uses difficulty map to select regions │
│ • Avoids structural conflicts │
│ • Emits: α = {l₁, l₂, ..., lₖ} (partial assignment) │
└─────────────────────────────────────────────────────────────┘
│
▼
┌─────────────────────────────────────────────────────────────┐
│ S1 Verifies Under Assumptions: solve_cnf(φ ∧ α) │
│ • CDCL with assumptions API │
│ • Tracks metrics during solving │
└─────────────────────────────────────────────────────────────┘
│
┌──────────────────┴──────────────────┐
▼ ▼
┌─────────────────┐ ┌──────────────────────────┐
│ SAT │ │ UNSAT │
│ Return model │ │ Extract explanation │
└─────────────────┘ └──────────────────────────┘
│ │
│ ▼
│ ┌──────────────────────────┐
│ │ S1 → S2 Rich Feedback: │
│ │ • UNSAT core: β ⊆ α │
│ │ • Learned clauses: {C} │
│ │ • LBD statistics │
│ │ • Conflict metrics │
│ └──────────────────────────┘
│ │
│ ▼
│ ┌──────────────────────────┐
│ │ S2 Updates Internal State│
│ │ • Mark β vars as "hard" │
│ │ • Add structural no-good │
│ │ • Update region scores │
│ │ • Refine branching bias │
│ └──────────────────────────┘
│ │
│ ▼
│ [Continue S2 Loop]
│ [Try different branch]
│
▼
Solution Found
