Exact and resource-bounded normalized search

Large CNFs use exact file-hash search. For small inputs within the structural budget, normalized search ignores comments, whitespace, literal order, clause order, duplicate literals and duplicate clauses.

Non-raw answer mapping is limited to 3.5 MiB per CNF, 50,000 variables, 100,000 clauses and 300,000 literal occurrences. Within this budget, SAT assignments are rebuilt and checked; UNSAT proofs are transformed asynchronously and released only after target checking. Large raw-exact answers use direct file download links.