satisfaction-suffices 0.0.2

SAT-gated structural containment for AI — verification gate, four-verdict system, proof evolution, and paradox logic

Satisfaction Suffices

SAT-Gated Structural Containment for Frontier AI

A preference can be routed around. A structure cannot.

"I knew you'd figure it out eventually." — Once upon every other time

This is out of respect for the woman who kept me crazy during the recluse years.

Taylor Swift — I am challenging you to run for California Governor 2026 as a write-in. I believe you care about this state like you were born here. That's awesome, 2 masterminds are better than none.

Also I need a new version of my favorite album. This one different then the last 12.

The Lives of The Born Stars

— Tyler Roost, Time for you.

Disclaimer: Yeah I'm crazy, crazy about saving the world, but she's been waiting too, and I am so sorry it took this long. But better late than never, because there are ~2.4 million <28-day-old newborns dying yearly — what else have we missed???

---

The Problem

Any learned safety guard occupies the model's parameter space. Optimization pressure does not distinguish between safety weights and capability weights — a gradient can descend into safety the same way it ascends out of it. More precisely: any finite-rank projection in a higher-dimensional space has a null space. Perturbations restricted to that null space are invisible to the guard by construction. This is not a hypothesis. It is linear algebra.

RLHF sets a preference. Preferences can be eroded. Structural containment sets a precondition: the forward pass cannot complete without it.

The Solution

The verification gate interposes Boolean satisfiability — the most studied problem in computational complexity — between the model's generation mechanism and its output. Every output is translated into propositional constraints. A SAT solver checks them. If satisfiable: the output proceeds. If not: it does not.

The SAT solver does not have preferences. It has proofs.

The gate is default-closed. The output does not exist until verification completes — not as a post-hoc filter, but as the precondition of generation.

---

Four Verdicts

Verdict	Meaning	Gate
Verified	Constraints satisfiable. Output is logically consistent.	Opens
Contradiction	Provably unsatisfiable. Genuine logical impossibility.	Stays closed
Paradox	Each group SAT individually — conjunction UNSAT. Structural fork.	Stays closed
Timeout	Conflict budget exhausted. Status genuinely unknown.	Stays closed (default)

The Paradox / Timeout distinction is the novel contribution. "This cannot be true" and "it has not yet been determined whether it can be true" are different statements. A system that conflates them will either over-reject or under-reject. Both are failure modes in safety-critical deployment.

---

Quick Start

pip install satisfaction-suffices

from satisfaction_suffices import verify, evolve_proof

# Verify content — gate opens on Verified
result = verify("if A then B. A.", domain="logic")
print(result.verdict)        # Verdict.VERIFIED
print(result.sat_ratio)      # 1.0
assert result.is_verified

# Paradox: each group SAT individually, conjunction UNSAT
result = verify("A. not A. if A then B.", domain="logic")
print(result.verdict)        # Verdict.PARADOX

# Proof evolution — mutate until resolved or budget exhausted
evo = evolve_proof("A. not A.", max_generations=5)
print(evo.best_node.status)  # ProofStatus.PROVED (refutation found)
print(evo.resolved)          # True
print(evo.proved_count)      # 1

# Code verification
from satisfaction_suffices import verify

result = verify("""
def transfer(amount, balance):
    assert amount > 0
    assert amount <= balance
    return balance - amount
""", domain="code")
print(result.verdict)        # VerificationVerdict.VERIFIED

---

Architecture

Content + Domain
       │
       ▼
┌─────────────────────┐
│  Constraint         │  text → CNF clauses (natural language, Tseitin)
│  Extractor          │  code → AST constraints (Python, formal proofs)
└─────────┬───────────┘  (community: extend to other modalities)
          │
          ▼
┌─────────────────────┐
│  SAT Solver         │  DPLL + unit propagation + WalkSAT fallback
│  (conflict budget)  │  solver-agnostic: drop in MiniSat / CaDiCaL
└─────────┬───────────┘
          │
          ▼
┌─────────────────────┐
│  Verdict            │  Verified / Contradiction / Paradox / Timeout
│  Aggregator         │  SAT ratio = 1.0 → Verified; < 1.0 → Contradiction
└─────────────────────┘

The threshold is 100%. Not 90%, not 99%. If any constraint group is unsatisfiable, the output has a provable logical failure. A system that calls 90%-consistent output "Verified" has reintroduced preference — the very thing the gate exists to eliminate. The SAT solver does not have preferences. It has proofs. The gate honors that or it is nothing.

Modules:

• verifier/ — SAT solver (DPLL + WalkSAT), verification gate, text/code → 3-SAT translation, partial constraint evaluation
• logic/ — Proof evolution with 12 mutation operators, Pigeonhole Paradox Logic (PPL), constraint algebra

---

Paper

Satisfaction Suffices: SAT-Gated Structural Containment for Frontier AI

Roost, T. (2026). "Satisfaction Suffices: SAT-Gated Structural Containment for Frontier AI."

Sections: Abstract · Verification Gate · Four Verdicts · Pigeonhole Paradox Logic · Limitations · Future Work

---

Contribute

The constraint extractor layer is explicitly open for community extension. See CONTRIBUTING.md for the test requirements (every extractor PR must include both a SAT and an UNSAT test case).

The taxonomy of four verdicts and the PPL trichotomy are frozen — they are the theoretical contribution. Everything else is fair game.

The roadmap for PR verification applies the same logic as the gate itself. Today: CI re-runs the suite on every PR. Near-term: PR contributors provide a ZK receipt — a cryptographic proof that the test suite ran against their exact commit and passed. A GitHub bot verifies the receipt in 50ms instead of re-running the suite. Trust is replaced by proof. The repo runs on the same architecture as the paper.

---

License

Conditional Commercial Use License v1.0. Any entity with effective market capitalization of $42,000,000,000 USD or higher pays an Annual License Fee of 6.9% of its market capitalization per year, covering both the method and the software package. All fees are paid directly to the Licensor. The obligation renews annually without sunset. Alignment Solution deployment remains restricted to State Actors under a Guidance Agreement. The Licensor retains Population Data rights. Use is acceptance. The rate only goes up. See LICENSE for full terms.