Metadata-Version: 2.4
Name: satisfiable-ai
Version: 0.1.0
Summary: HuggingFace dataset wrappers for SAT-verified training data
Author: TimeLordRaps
License: CCUL v1.0
Project-URL: Homepage, https://github.com/TimeLordRaps/satisfiable-ai
Project-URL: Repository, https://github.com/TimeLordRaps/satisfiable-ai
Project-URL: Issues, https://github.com/TimeLordRaps/satisfiable-ai/issues
Project-URL: Changelog, https://github.com/TimeLordRaps/satisfiable-ai/releases
Keywords: sat,verification,ai-safety,datasets,huggingface,curriculum
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: Python :: 3
Classifier: Topic :: Scientific/Engineering :: Artificial Intelligence
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: satisfaction-suffices>=0.0.1
Provides-Extra: dev
Requires-Dist: pytest>=7.0; extra == "dev"
Requires-Dist: pytest-cov>=4.0; extra == "dev"
Provides-Extra: torch
Requires-Dist: torch>=2.0; extra == "torch"
Provides-Extra: datasets
Requires-Dist: datasets>=2.18; extra == "datasets"
Provides-Extra: all
Requires-Dist: torch>=2.0; extra == "all"
Requires-Dist: datasets>=2.18; extra == "all"
Dynamic: license-file

# satisfiable-ai

[![CI](https://github.com/TimeLordRaps/satisfiable-ai/actions/workflows/ci.yml/badge.svg)](https://github.com/TimeLordRaps/satisfiable-ai/actions/workflows/ci.yml)
[![PyPI version](https://img.shields.io/pypi/v/satisfiable-ai.svg)](https://pypi.org/project/satisfiable-ai/)
[![License: CCUL v1.0](https://img.shields.io/badge/License-CCUL%20v1.0-blueviolet.svg)](./LICENSE)
[![Python 3.10+](https://img.shields.io/badge/python-3.10%2B-blue.svg)](https://www.python.org/downloads/)

**HuggingFace dataset wrappers for SAT-verified training data.**

Every training sample passes through a SAT verification gate before entering any pipeline. Only logically consistent samples survive. Built on [`satisfaction-suffices`](https://github.com/TimeLordRaps/satisfaction-suffices).

---

## Critical Path

![Critical execution path](docs/flow.svg)

---

## Read This First

| Time | What you get |
|---|---|
| **30 seconds** | What this is and why it exists |
| **60 seconds** | Why verified training data matters |
| **2 minutes** | How to hook in a transformers architecture |
| **10 minutes** | Full architecture + curriculum system |
| **15.5 minutes** | Training on the four-verdict signal as frontier detection |

---

### ⏱ 30 seconds

Models trained on logically inconsistent data learn inconsistent reasoning. This library filters every training sample through a SAT verification gate — the same gate from `satisfaction-suffices` — before it enters your pipeline. Only verified samples survive by default.

---

### ⏱ 60 seconds

Current safety training (RLHF, DPO) adjusts output *distribution*. It does not verify logical *consistency*. A model can learn to sound safe while reasoning incorrectly.

Training on SAT-verified data builds a model whose training distribution is structurally consistent. Every sample that reached it passed a proof. The model learns from a population that couldn't contradict itself.

---

### ⏱ 2 minutes — Hook into transformers

```python
from satisfiable_ai import VerifiedDataset, default_schedule

# Filter your data to SAT-verified samples only
dataset = VerifiedDataset(
    samples=your_data,   # list of {"text": "..."} dicts
    domain="logic",      # "logic" | "code" | "math" | "proof"
    strict=True,         # True = only VERIFIED; False = exclude CONTRADICTION only
)

# Curriculum scheduling — staggers complexity across training phases
schedule = default_schedule()
# schedule.phases: Foundation → Execution → Domain → Consolidate
# Feed each phase to your HuggingFace Trainer as a separate training stage

for phase in schedule.phases:
    trainer.train_dataset = phase.sources
    trainer.train()
```

The four verdict classes are available as labels if you want to train on the full signal:

```python
from satisfiable_ai import verify
result = verify("if A then B. A. therefore B.", domain="logic")
# result.verdict: "VERIFIED" | "CONTRADICTION" | "PARADOX" | "TIMEOUT"
# result.sat_ratio: float — fraction of constraint groups that resolved satisfiable
```

---

### ⏱ 10 minutes

**Architecture:**

```
satisfiable-ai
├── satisfiable_ai/
│   ├── dataset_builder/
│   │   ├── sources.py      — HuggingFace dataset registry
│   │   ├── curriculum.py   — phase scheduling (Foundation → Execution → Domain → Consolidate)
│   │   └── runtime.py      — VerifiedDataset / StreamingVerifiedDataset (requires torch)
│   ├── verifier/           — imported from satisfaction-suffices
│   │   ├── sat.py          — DPLL solver with WalkSAT fallback
│   │   ├── verify.py       — gate: extract → solve → aggregate → verdict
│   │   └── partial.py      — prefix feasibility for streaming use
│   └── __init__.py         — public API surface
```

**Install:**

```bash
pip install satisfiable-ai
# with torch:
pip install "satisfiable-ai[torch]"
```

**Verdict reference:**

| Verdict | Meaning | Default behavior |
|---|---|---|
| VERIFIED | Constraints satisfiable, gate opens | Include in training data |
| CONTRADICTION | Provably impossible | Exclude (strict and non-strict) |
| PARADOX | Each clause valid, conjunction unsatisfiable | Exclude (use as evolution seed) |
| TIMEOUT | Solver budget exhausted, verdict unknown | Exclude in strict mode |

---

### ⏱ 15.5 minutes — Training on the frontier

The four verdict classes are not just filters. They are training signal.

**Verdict-conditioned training:** label each sample with its verdict and train the model to predict verdict alongside output. A model that can predict whether its own output is VERIFIED, PARADOX, or TIMEOUT is building an internal model of its logical boundary.

**Timeout as emergence detector:** The 3-SAT phase transition concentrates solver timeouts at clause/variable ratio ~4.267. As a model's outputs grow more complex, timeout density in your verification pass may spike before capability emergence is otherwise measurable. Monitor `result.sat_ratio` distributions across training checkpoints.

**Paradox curriculum:** PARADOX samples — individually satisfiable clauses that are jointly unsatisfiable — represent the structural frontier of the model's current reasoning. Feed them back as the hardest curriculum stage. The model learns to recognize the shape of its own inconsistency boundaries.

For the full theoretical grounding, read the paper in [`satisfaction-suffices/paper/paper_01_submission.md`](https://github.com/TimeLordRaps/satisfaction-suffices/blob/main/paper/paper_01_submission.md).

---

## License

AGPL-3.0-or-later
