Stop the scout gate from discarding coupled-frame results; include unit clauses in the 2-SAT check

backend/binary_clause_check.py

@@ -25,8 +25,12 @@
 proof of UNSAT from the binary clauses alone, independent of Kissat,
 independent of DRAT/proof-checker availability.
 
-Scope: this only inspects 2-literal clauses. A formula can be
-consistent on its binary clauses but still UNSAT overall (the
+Unit clauses (a) are folded in as (a OR a), i.e. the single edge
+not(a) -> a, so chains like x1, x1->x2->...->xn, not(xn) are refuted
+too; an empty clause is reported inconsistent outright.
+
+Scope: this only inspects clauses of at most 2 literals. A formula can be
+consistent on those clauses but still UNSAT overall (the
 contradiction may only emerge from longer clauses) - in that case this
 reports "consistent" and simply doesn't apply. It is a sound partial
 certificate for UNSAT, not a full decision procedure.
@@ -46,8 +50,11 @@ class BinaryClauseCheckResult:
 
     consistent: bool
     num_binary_clauses: int
-    #: 1-indexed variable forced to be both true and false; set iff not consistent
+    #: 1-indexed variable forced to be both true and false; set when not
+    #: consistent, except when the conflict is an empty clause (then None)
     conflicting_variable: Optional[int] = None
+    #: number of unit clauses folded into the implication graph
+    num_unit_clauses: int = 0
 
 
 def _literal_node(lit: int) -> int:
@@ -108,20 +115,30 @@ def _kosaraju_scc(graph: List[List[int]], num_nodes: int) -> List[int]:
 
 
 def check_binary_clauses(formula: CNFFormula) -> BinaryClauseCheckResult:
-    """Check whether the formula's 2-literal clauses are jointly consistent.
+    """Check whether the formula's clauses of <= 2 literals are jointly consistent.
 
     Args:
-        formula: CNF formula (only its binary clauses are inspected)
+        formula: CNF formula (only its empty, unit and binary clauses are inspected)
 
     Returns:
         BinaryClauseCheckResult; `consistent=False` is a sound proof that
         the whole formula is UNSAT (a necessary sub-constraint already
         fails), independent of Kissat or proof checking.
     """
     binary_clauses = [c for c in formula.clauses if len(c) == 2]
+    unit_clauses = [c for c in formula.clauses if len(c) == 1]
     num_nodes = 2 * formula.num_vars
 
+    if any(len(c) == 0 for c in formula.clauses):
+        return BinaryClauseCheckResult(
+            consistent=False,
+            num_binary_clauses=len(binary_clauses),
+            num_unit_clauses=len(unit_clauses),
+        )
+
     graph: List[List[int]] = [[] for _ in range(num_nodes)]
+    for (a,) in unit_clauses:                       # (a) == (a OR a): not(a) -> a
+        graph[_negate_node(_literal_node(a))].append(_literal_node(a))
     for clause in binary_clauses:
         a, b = clause
         na = _negate_node(_literal_node(a))
@@ -137,9 +154,11 @@ def check_binary_clauses(formula: CNFFormula) -> BinaryClauseCheckResult:
                 consistent=False,
                 num_binary_clauses=len(binary_clauses),
                 conflicting_variable=v,
+                num_unit_clauses=len(unit_clauses),
             )
 
     return BinaryClauseCheckResult(
         consistent=True,
         num_binary_clauses=len(binary_clauses),
+        num_unit_clauses=len(unit_clauses),
     )

backend/frame_solver.py

@@ -322,31 +322,46 @@ def frame_solve_coupled(formula: CNFFormula, max_rounds: int = 64) -> CoupledRes
 # tunnel at ~3.3x speedup. The Charter way: the cheaper detector wins, measured.
 # --------------------------------------------------------------------------
 def _no_exploitable_structure(formula: CNFFormula, xr: XORExtractionResult) -> bool:
-    """Cheap sufficient condition for TUNNEL: no XOR groups AND no pigeonhole-shaped
-    counting structure (an all-positive ALO clause together with a negative-binary
-    AMO clause). When both are absent, neither the parity nor the counting frame can
-    bite, and with the 2-SAT frame already consistent the coupling cannot either --
-    so the coupled router would punt to CDCL anyway, only after wasted work."""
+    """Cheap sufficient condition for TUNNEL: none of the coupled router's moves can
+    bite. Requires ALL of:
+
+    - no XOR groups (the parity frame and parity propagation are empty);
+    - no unit clauses (with no units, unit propagation over the <=2-literal
+      clauses pins nothing, so the coupling has no entailed literals to exchange
+      -- a unit chain like x1, x1->...->xn, not(xn) is decided by that BCP);
+    - at least one all-positive clause (otherwise the coupling's all-False
+      completion already satisfies the formula and it would return SAT);
+    - no pigeonhole-shaped counting structure (an all-positive ALO clause together
+      with a negative-binary AMO clause).
+
+    When all hold, and the 2-SAT frame is already consistent, frame_solve_coupled
+    would punt to CDCL anyway, only after wasted work."""
     if xr.xors:
         return False
-    has_alo = any(c and all(l > 0 for l in c) for c in formula.clauses)
+    if any(len(c) <= 1 for c in formula.clauses):
+        return False
+    has_alo = any(all(l > 0 for l in c) for c in formula.clauses)
+    if not has_alo:
+        return False
     has_amo = any(len(c) == 2 and c[0] < 0 and c[1] < 0 for c in formula.clauses)
-    return not (has_alo and has_amo)
+    return not has_amo
 
 
 def frame_solve_scouted(formula: CNFFormula, use_scout: bool = True) -> CoupledResult:
     """Structure-gated coupled router. Same certified SAT/UNSAT verdicts as
-    `frame_solve_coupled`, but on a cheap TUNNEL signal (no XOR and no counting
-    structure) it skips the algebraic pre-pass and reports CDCL_NEEDED immediately
-    -- removing the wasted parity/coupling work on structureless instances
-    (measured ~3.3x faster on random-3SAT).
+    `frame_solve_coupled`, but on a cheap TUNNEL signal (no XOR, no unit clauses,
+    an all-positive clause, and no counting structure) it skips the algebraic
+    pre-pass and reports CDCL_NEEDED immediately -- removing the wasted
+    parity/coupling work on structureless instances (measured ~3.3x faster on
+    random-3SAT).
 
     Soundness: the gate only ever short-circuits the CDCL_NEEDED *punt* (which
     frame_solve_coupled also returns on these instances, just after more work); it
     never turns a frame SAT/UNSAT into a punt. The 2-SAT frame (near-free, sound) is
-    always taken first, and any XOR- or counting-shaped instance fails the gate and
-    gets the full coupling. Differential-tested against frame_solve_coupled
-    (0 verdict mismatches, 0 frame-wins lost) in tests/test_frame_solver.py."""
+    always taken first, and any XOR-, unit- or counting-shaped instance (or one the
+    all-False completion satisfies) fails the gate and gets the full coupling.
+    Differential-tested against frame_solve_coupled (0 verdict mismatches, 0
+    frame-wins lost) in tests/test_frame_solver.py."""
     if not check_binary_clauses(formula).consistent:
         return CoupledResult('UNSAT', '2sat', True, None, 0, 0)
     if use_scout and _no_exploitable_structure(formula, extract_xors(formula)):

backend/tests/test_binary_clause_check.py

@@ -79,3 +79,29 @@ def test_self_conflicting_unit_pair(self):
         result = check_binary_clauses(cnf)
         assert result.consistent is False
         assert result.conflicting_variable == 1
+
+    def test_unit_clauses_refute_implication_chain(self):
+        # x1, x1 -> x2 -> ... -> x5, ¬x5: units folded in as ¬a -> a edges
+        n = 5
+        clauses = [[1]] + [[-i, i + 1] for i in range(1, n)] + [[-n]]
+        result = check_binary_clauses(CNFFormula(num_vars=n, clauses=clauses))
+        assert result.consistent is False
+        assert result.conflicting_variable is not None
+        assert result.num_unit_clauses == 2
+        assert result.num_binary_clauses == n - 1
+
+    def test_contradictory_units(self):
+        result = check_binary_clauses(CNFFormula(num_vars=1, clauses=[[1], [-1]]))
+        assert result.consistent is False
+        assert result.conflicting_variable == 1
+
+    def test_consistent_units(self):
+        cnf = CNFFormula(num_vars=3, clauses=[[1], [-1, 2], [-3]])
+        result = check_binary_clauses(cnf)
+        assert result.consistent is True
+        assert result.num_unit_clauses == 2
+
+    def test_empty_clause_is_inconsistent(self):
+        result = check_binary_clauses(CNFFormula(num_vars=2, clauses=[[1, 2], []]))
+        assert result.consistent is False
+        assert result.conflicting_variable is None

backend/tests/test_frame_solver.py

@@ -340,6 +340,28 @@ def test_gate_keeps_structured_wins(self):
         assert frame_solve_scouted(_tseitin_k4()).status == "UNSAT"
         assert frame_solve_scouted(pigeonhole(6)[0]).status == "UNSAT"
 
+    def test_gate_keeps_unit_chain_refutation(self):
+        # x1, x1 -> ... -> xn, ¬xn: must be refuted, never punted to CDCL
+        for n in (2, 5, 30):
+            clauses = [[1]] + [[-i, i + 1] for i in range(1, n)] + [[-n]]
+            f = CNFFormula(num_vars=n, clauses=clauses)
+            assert frame_solve_coupled(f).status == "UNSAT"
+            assert frame_solve_scouted(f).status == "UNSAT"
+
+    def test_gate_keeps_unit_driven_wide_clause_refutation(self):
+        # units pin x1..x3 false, falsifying the wide clause (x1 v x2 v x3):
+        # 2-SAT is consistent, but the coupling's BCP + simplify refutes it
+        f = CNFFormula(num_vars=3, clauses=[[-1], [-2], [-3], [1, 2, 3]])
+        assert frame_solve_coupled(f).status == "UNSAT"
+        assert frame_solve_scouted(f).status == "UNSAT"
+
+    def test_gate_keeps_all_false_sat(self):
+        # every clause has a negative literal: the all-False completion is a model
+        f = CNFFormula(num_vars=4, clauses=[[1, 2, -3], [-1, 3, 4], [2, -4, 3]])
+        assert frame_solve_coupled(f).status == "SAT"
+        sc = frame_solve_scouted(f)
+        assert sc.status == "SAT" and verify_model(f, sc.model)
+
 
 def _has_model(f: CNFFormula) -> bool:
     """Brute-force satisfiability check for small formulas (test oracle)."""

docs/ladder/scripts/cosmo_map.py

@@ -71,7 +71,7 @@
 
 def _twosat_contradiction(k: int) -> CNFFormula:
     """Pure-BINARY 2-SAT contradiction (check_binary_clauses inspects only
-    2-literal clauses, so the certificate must live there). The core forces
+    clauses of <= 2 literals, so the certificate must live there). The core forces
     a <-> ¬a: a->b->¬a and ¬a->¬b->a put a and ¬a in one SCC. Extra variables
     are chained strongly-connected to grow the size axis without changing the
     verdict."""