torc-sat 0.1.1

Topological SAT preprocessor — detects UNSAT via cohomological obstructions

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

pip install -e .

Usage

CLI

# 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

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.