Merge pull request #32 from jesusvilela/codex/revisar-y-evaluar-contra-sota-2026

Remove C++/Cython tribridge; add Python fallbacks and spectral features; simplify CLI/bench APIs

Author: jesusvilela

.gitignore

@@ -43,6 +43,3 @@ docs/ladder/scripts/*_results.json
 build/
 dist/
 __pycache__/
-*.pyd
-*.obj
-build/

README.md

@@ -1,9 +1,5 @@
 # λSAT · the moving frame
 
-![Canary Springtime Path](docs/assets/canary_path.png)
-> *The path has chosen you, now you honour the springtime in the pathwalk.*
-> **CANARY REPOSITORY:** This is the experimental, formalized structure of the solver.
-
 > *A solver that carries its own proof, and knows which shape of hardness it's looking at.*
 
 [![tests](https://github.com/jesusvilela/lambda-sat-solver/actions/workflows/tests.yml/badge.svg)](https://github.com/jesusvilela/lambda-sat-solver/actions/workflows/tests.yml)
@@ -85,30 +81,43 @@ where game theory flips: on the island a *pure* strategy dominates; on the tunne
 
 ---
 
-## 構造 · the Canary stack (Adiabatic Geodesic Flow)
-
-The Canary architecture wholly abandons heuristic python string-matching and scalar Euclidean approximations (like simplistic `m/n` clause-ratio checks). Instead, it physicalizes the solver as a Hamiltonian system operating under hyper-dimensional Riemannian logic. Every layer is mapped directly to a structural C++ topology extractor, bridging discrete logic into a continuous Riemannian manifold.
+## 構造 · the stack
 
-> **Read the full philosophical and mathematical integration:** [The Ultimate Synthesis](ultimate_synthesis.md)
+Every layer is the same operator seen at a different scale. Fractal, self-similar, and
+each verdict certified all the way down.
 
 ```mermaid
-graph TD
-    A[CNF Hyper-Manifold] --> B(C++ Tensor-Native Flavor Analyzer)
-    B -- O(L) Dense SIMD Vectorization --> C{Cython Topological Bridge}
-    C -- Z2 x Z2 Parity Matrix --> D[Bridge Annealer: Parity Oracle]
-    C -- A4 High-Density Topology --> E[Bridge Annealer: CMS Gauss-Jordan]
-    C -- Trivial/Unstructured Geometry --> F[CDCL Fallback / Bare Kissat]
-    D --> G(Diamond Holonomy Verification in Lean 4)
-    E --> G
-    F --> G
+flowchart TD
+    ACAF["<b>ACAF</b> · adaptive actor-critic-ambigator-fuzzer"] --> META["<b>metasolver</b> · description-driven dispatch"]
+    ACAF --> MM["<b>meta-metasolver</b> · fractal seed-portfolio"]
+    META --> FR["<b>frame router</b> · 3 sound frames + Nelson-Oppen coupling"]
+    MM --> FR
+    META --> K["certified CDCL · Kissat / CaDiCaL"]
+    MM --> K
+    FR --> OBS(["<b>observer</b> — certify every verdict"])
+    K --> OBS
+
+    DESC["<b>the view from outside</b><br/>dynamics · fabric · hyperbolic model"] -.reads.-> ACAF
 ```
 
-- **Flavor Analyzer** (`backend/cpp/flavor_analyzer.hpp`) — C++ structural extractor. Reads the exact hyper-dimensional geometry of the CNF to map dispersion groups ($Z_2 \times Z_2$, $A_4$, Trivial).
-- **Cython Bridge** (`backend/cython/tribridge.pyx`) — Lifts the C++ `vector[vector[int]]` geometry into the Python space seamlessly.
-- **BBD Router** (`backend/cpp/router.hpp`) — Breathing Bridge Descent. Selects the geodesic path instantly based on the Flavor group, acting as a Hamiltonian state transition rather than a heuristic choice. It rejects Euclidean scalars in favor of topological shape-matching (e.g., verifying exact variable overlap for XOR expansion).
-- **Parity Oracle** — Handles highly structured cryptographic chains with zero search.
-- **CDCL Fallback** (`Kissat/CaDiCaL`) — The unstructured heavy-tail engine.
-- **Diamond Holonomy Benchmarking** — Evaluates paths using rigorous TFLOPS-bounded physics instead of scalar time.
+- **frame router** (`frame_solver.py`) — the three frames + their coupling, refute-first.
+- **metasolver** (`metasolver.py`) — reverts the dynamical description into a dispatch. On a
+  *counting-and-parity-inclusive mix* (not the competition set) it wins on PAR-2 over Kissat,
+  CaDiCaL and CryptoMiniSat — because it is instant where they blow up on counting, and
+  comparable elsewhere. A structural result on a specific mix, not a generally faster solver.
+- **meta-metasolver** (`metametasolver.py`) — the minimax mixed strategy; on the heavy-tailed
+  random-3SAT band it *out-searches CMS in wall-clock* (parallel, at a `k×` CPU cost, no CMS
+  in the pool). Single-thread on few cores, this advantage shrinks — see the honest scope.
+- **metasolver** (`metasolver.py`) — description-driven dispatch. On the included
+  competition-style mix, its aggregate win comes from routing structured islands before
+  CDCL, not from a claim of general CDCL dominance.
+- **meta-metasolver** (`metametasolver.py`) — seed-diversified CDCL portfolio for the
+  heavy-tailed random-3SAT band; measured in the repo's scoped benchmark, with CPU cost
+  reported.
+- **ACAF** (`acaf.py`) — sizes the mixed strategy to the cores; wins the structured tier by
+  a constructive certificate, the hard tier by an adaptive portfolio.
+- **the view from outside** — `dynamics.py` (laws/relations/motions), `fabric.py` +
+  `fabric_model.py` (the hyperbolic instance-manifold), `observer.py` (the adjudicator).
 
 > Every number here is a *measured* claim on a small, fixed, synthetic mix — regenerate it
 > with one command and read the scope in [`REPRODUCIBILITY.md`](REPRODUCIBILITY.md). This is
@@ -145,13 +154,6 @@ python -m backend.cli examples/simple_sat.cnf --heuristic aggressive
 python -m pytest backend/tests/ -q
 ```
 
-### Benchmarking against SAT Competition
-To operationalize the solver and squeeze performance on standard competition instances (`.cnf`, `.xz`, `.lzma`):
-
-```bash
-python -m backend.benchmark_cli ./cache/zenodo_full/ --pattern "*.xz" --timeout 5000 --parallel
-```
-
 Strict certification smoke tests:
 
 ```bash

backend/acaf.py

@@ -61,22 +61,11 @@ def _critic(formula: CNFFormula) -> Tuple[bool, float, int]:
     dyn = describe(formula)
     if dyn.certified:
         return True, 0.0, len(dyn.conserved)
-        
-    hardness = 1.0  # default to heavy tail
-    ambiguity = 0
-    try:
-        from .cython import tribridge
-        res = tribridge.route_instance_topology(formula.clauses, formula.num_vars)
-        struct_class = res["class"]
-        
-        # PURE_GF2 and PARTIAL_XOR_SADDLE have bounded tails, they don't need swarm
-        if struct_class in ("PURE_GF2", "PARTIAL_XOR_SADDLE"):
-            hardness = 0.0
-            ambiguity = 1
-    except ImportError:
-        pass
-        
-    return False, hardness, ambiguity
+    n = max(formula.num_vars, 1)
+    # random-3SAT gets into the heavy-tailed seconds regime past ~220 vars (measured);
+    # a smooth proxy, saturating, cheap -- no solve required.
+    hardness = min(1.0, n / 260.0)
+    return False, hardness, 0
 
 
 # ---- FUZZER: generate decorrelated engine+seed configs ----
@@ -113,7 +102,7 @@ def acaf_solve(formula: CNFFormula, timeout_s: float = 30.0,
             return ACAFResult("SAT", time.perf_counter() - t0, "frame",
                               r.resolved_by, True, model=r.model, hardness=0.0)
         # frame check said suffice but punted (rare) -> fall through to tunnel policy
-        _, hardness, _ = _critic(formula)
+        hardness = min(1.0, max(formula.num_vars, 1) / 260.0)
 
     cores = _cores()
     # AMBIGATOR: size the diversification to the predicted tail weight, capped at cores.

backend/benchmark.py

@@ -438,26 +438,20 @@ def compare_configs(self, config1: str, config2: str) -> Dict[str, Any]:
         }
 
 
-def discover_benchmarks(directory: Path, pattern: str | List[str] = "*.cnf") -> List[BenchmarkInstance]:
+def discover_benchmarks(directory: Path, pattern: str = "*.cnf") -> List[BenchmarkInstance]:
     """
     Discover benchmark instances in a directory
 
     Args:
         directory: Directory to search
-        pattern: File pattern to match or list of patterns (default: *.cnf)
+        pattern: File pattern to match (default: *.cnf)
 
     Returns:
         List of benchmark instances
     """
     instances = []
-    
-    if isinstance(pattern, str):
-        patterns = [pattern]
-    else:
-        patterns = pattern
-
-    for p in patterns:
-        for path in directory.rglob(p):
+
+    for path in directory.rglob(pattern):
         # Try to infer category from directory structure
         category = path.parent.name if path.parent != directory else "unknown"
 

backend/benchmark_cli.py

@@ -25,9 +25,8 @@ async def main():
 
     parser.add_argument(
         '--pattern',
-        nargs='+',
-        default=['*.cnf', '*.xz', '*.lzma'],
-        help='File patterns to match (default: *.cnf *.xz *.lzma)'
+        default='*.cnf',
+        help='File pattern to match (default: *.cnf)'
     )
 
     parser.add_argument(

backend/cnf_profile.py

@@ -59,7 +59,86 @@ def _clause_is_horn(clause) -> bool:
     return sum(1 for lit in clause if lit > 0) <= 1
 
 
+def _shannon_entropy_ratio(weights) -> Optional[float]:
+    """Normalized Shannon entropy of a nonnegative weight vector.
 
+    Returns H(p) / log(n) in [0, 1], where p is the weight vector
+    normalized to sum to 1. Returns None if there are fewer than 2
+    nonzero weights (entropy is degenerate/undefined as a ratio).
+    """
+    total = sum(weights)
+    if total <= 0:
+        return None
+    nonzero = [w for w in weights if w > 0]
+    if len(nonzero) < 2:
+        return None
+    probs = [w / total for w in nonzero]
+    h = -sum(p * math.log(p) for p in probs)
+    return h / math.log(len(nonzero))
+
+
+def _hyperbolic_delta_entropy_ratio(
+    formula: CNFFormula,
+) -> Optional[float]:
+    """Experimental spectral feature: see `CNFProfile.hyp_delta_entropy_ratio`.
+
+    Builds the signed clause-variable incidence matrix M (clauses x vars,
+    M[c, v] = +1 / -1 / 0 for the polarity of variable v in clause c),
+    computes the normalized entropy of its singular-value distribution,
+    then repeats after mapping each row through the Poincare-ball
+    exponential map at the origin (a standard hyperbolic embedding:
+    exp_0(x) = tanh(||x||) * x / ||x||, applied after scaling rows to
+    unit max-norm so the map is well-defined). Returns hyp - euclidean.
+    """
+    try:
+        import numpy as np
+    except ImportError:
+        return None
+
+    n_vars = formula.num_vars
+    n_clauses = formula.num_clauses
+    if n_vars == 0 or n_clauses == 0:
+        return None
+    if n_vars * n_clauses > _SVD_MAX_CELLS:
+        return None
+
+    matrix = np.zeros((n_clauses, n_vars), dtype=np.float64)
+    for i, clause in enumerate(formula.clauses):
+        for lit in clause:
+            v = abs(lit) - 1
+            if 0 <= v < n_vars:
+                matrix[i, v] = 1.0 if lit > 0 else -1.0
+
+    def entropy_ratio_of(m: "np.ndarray") -> Optional[float]:
+        try:
+            singular_values = np.linalg.svd(m, compute_uv=False)
+        except np.linalg.LinAlgError:
+            return None
+        return _shannon_entropy_ratio(singular_values.tolist())
+
+    euclidean_ratio = entropy_ratio_of(matrix)
+    if euclidean_ratio is None:
+        return None
+
+    row_norms = np.linalg.norm(matrix, axis=1, keepdims=True)
+    max_norm = row_norms.max()
+    if max_norm <= 0:
+        return None
+    normalized = matrix / max_norm
+    row_norms_normalized = np.linalg.norm(normalized, axis=1, keepdims=True)
+    with np.errstate(invalid='ignore', divide='ignore'):
+        scale = np.where(
+            row_norms_normalized > 0,
+            np.tanh(row_norms_normalized) / row_norms_normalized,
+            0.0,
+        )
+    hyperbolic = normalized * scale
+
+    hyperbolic_ratio = entropy_ratio_of(hyperbolic)
+    if hyperbolic_ratio is None:
+        return None
+
+    return hyperbolic_ratio - euclidean_ratio
 
 
 def profile_cnf(formula: CNFFormula, compute_spectral: bool = True) -> CNFProfile:
@@ -110,8 +189,12 @@ def profile_cnf(formula: CNFFormula, compute_spectral: bool = True) -> CNFProfil
     pos_neg_balance = num_positive_lits / total_lits if total_lits else 0.5
     avg_var_degree = total_lits / num_vars if num_vars else 0.0
 
-    # SVD entropy ratio previously removed
-    var_degree_entropy = 0.0
+    degree_entropy_ratio = _shannon_entropy_ratio(var_degree[1:])
+    var_degree_entropy = degree_entropy_ratio if degree_entropy_ratio is not None else 0.0
+
+    hyp_delta = None
+    if compute_spectral:
+        hyp_delta = _hyperbolic_delta_entropy_ratio(formula)
 
     return CNFProfile(
         num_vars=num_vars,
@@ -123,5 +206,5 @@ def profile_cnf(formula: CNFFormula, compute_spectral: bool = True) -> CNFProfil
         pos_neg_balance=pos_neg_balance,
         avg_var_degree=avg_var_degree,
         var_degree_entropy=var_degree_entropy,
-        hyp_delta_entropy_ratio=None,
+        hyp_delta_entropy_ratio=hyp_delta,
     )

backend/cnf_utils.py

@@ -158,16 +158,10 @@ def parse_dimacs(text: str, strict: bool = False) -> CNFFormula:
     )
 
 
-import lzma
-
 def parse_dimacs_file(path: Path, strict: bool = False) -> CNFFormula:
-    """Parse DIMACS CNF file (supports .cnf, .xz, .lzma)"""
-    if path.suffix in ['.xz', '.lzma']:
-        with lzma.open(path, 'rt') as f:
-            return parse_dimacs(f.read(), strict=strict)
-    else:
-        with open(path, 'r') as f:
-            return parse_dimacs(f.read(), strict=strict)
+    """Parse DIMACS CNF file"""
+    with open(path, 'r') as f:
+        return parse_dimacs(f.read(), strict=strict)
 
 
 def write_dimacs(formula: CNFFormula, path: Path):