Metadata-Version: 2.4
Name: torc-sat
Version: 0.1.1
Summary: Topological SAT preprocessor — detects UNSAT via cohomological obstructions
Author-email: Carmen Esteban <caresment@gmail.com>
License: All Rights Reserved
Keywords: SAT,topology,cohomology,UNSAT,preprocessor
Classifier: Development Status :: 3 - Alpha
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Programming Language :: Python :: 3
Requires-Python: >=3.9
Description-Content-Type: text/markdown
Requires-Dist: numpy>=1.21
Requires-Dist: python-sat>=0.1.8
Provides-Extra: benchmark
Requires-Dist: cnfgen; extra == "benchmark"
Provides-Extra: dev
Requires-Dist: pytest>=7.0; extra == "dev"

# torc-sat

Topological SAT preprocessor. Detects UNSAT in CNF formulas via cohomological obstructions.

First-of-its-kind: recognizes combinatorial structures (PHP, Tseitin, graph coloring) hidden in DIMACS CNF and applies TORC topological infeasibility certificates. Returns UNSAT with mathematical proof or UNKNOWN (pass to SAT solver).

## Install

```bash
pip install -e .
```

## Usage

### CLI

```bash
# Check a single instance
torc-sat check instance.cnf

# JSON output
torc-sat check instance.cnf --json

# Benchmark a directory
torc-sat bench benchmark/instances/
```

### Python API

```python
from torc_sat import check

result = check("instance.cnf")
print(result.verdict)       # UNSAT or UNKNOWN
print(result.time_ms)       # milliseconds
print(result.certificate)   # topological certificate (if UNSAT)
```

## Supported structures

| Structure | Detection | TORC method | Typical speedup vs SAT solver |
|-----------|-----------|-------------|-------------------------------|
| PHP(n+1,n) | Pigeon + hole clauses | Cech H1 cohomology | >1000x for n>15 |
| Tseitin | XOR groups | GF(2) rank obstruction | >100x |
| Graph coloring | At-least-one + conflict | Clique lower bound | >50x |

## Soundness

TORC never produces false positives. If it says UNSAT, it IS unsat (mathematical proof). If it says UNKNOWN, pass to a SAT solver.

## License

All Rights Reserved. Carmen Esteban / IAFISCAL & PARTNERS.
