[Copilot]

frame_solve_scouted returned CDCL_NEEDED on unit chains like x1, x1→…→xn, ¬xn, which frame_solve_coupled refutes. Separately, check_binary_clauses ignored unit clauses, so it missed easy refutations.

n = 5
f = CNFFormula(num_vars=n, clauses=[[1]] + [[-i, i+1] for i in range(1, n)] + [[-n]])
frame_solve_coupled(f).status   # 'UNSAT'
frame_solve_scouted(f).status   # before: 'CDCL_NEEDED'   after: 'UNSAT'

Scout gate (_no_exploitable_structure)

• Old gate: it sent a formula to CDCL whenever there was no XOR or pigeonhole structure. That ignored two other ways the coupled router decides formulas:
  • Unit propagation over clauses of ≤2 literals, which can fix variables and then refute or falsify a longer clause.
  • The all-False assignment, which the coupled router tries and returns as SAT if it satisfies the formula.
• New gate: it skips to CDCL only when all of these hold:
  • no XORs
  • no clauses with ≤1 literal
  • at least one all-positive clause
  • no pigeonhole shape (ALO + negative-binary AMO)
• Result: with these conditions, the gate fires only on formulas where frame_solve_coupled would also return CDCL_NEEDED. The docstring's "never loses a frame win" claim is now true by construction, not just on the differential corpus.
• Random 3-SAT: it has no unit clauses and almost always has an all-positive clause, so the shortcut should still fire there. I have not re-run the ~3.3x benchmark.

check_binary_clauses

• A unit clause (a) is added as (a ∨ a), i.e. the single edge ¬a → a. This is still sound, and it lets every router refute the chain above at the 2-SAT step.
• An empty clause makes the result inconsistent. conflicting_variable is None in that case.
• New field BinaryClauseCheckResult.num_unit_clauses (default 0). Existing callers only read .consistent.

Tests

• test_binary_clause_check.py:
  • a unit-driven chain
  • contradictory units
  • consistent units
  • an empty clause
• TestScoutedGate:
  • unit chains with n = 2, 5, 30
  • units that falsify a wide clause
  • a formula the all-False assignment satisfies, which should return SAT rather than CDCL_NEEDED