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

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.