Type Alias: ProofExportResult
@kortexya/reasoninglayer / ProofEngine / ProofExportResult
Type Alias: ProofExportResult
ProofExportResult =
"unsatisfiable"|"satisfiable"|"unknown"
Defined in: src/types/proof-engine.ts:492
The solver’s verdict on the submitted CNF.
Remarks
unknown means the conflict budget (maxConflicts) was exhausted before a verdict
was reached. A certificate is exported only for unsatisfiable — a satisfiable
formula has no refutation.
Example
const result: ProofExportResult = 'unsatisfiable';