Interface: SatUnsatisfiableResult

@kortexya/reasoninglayer / Sat / SatUnsatisfiableResult

Interface: SatUnsatisfiableResult

Defined in: src/types/sat.ts:149

Result of a SAT solve where the formula was proven unsatisfiable.

Remarks

No model is produced. The solver does not return an unsat core over this endpoint; DRAT proof logging (SatSolveRequest.proofLogging) only affects server-side proof emission.

Example

if (response.result === 'unsatisfiable') {
  console.log(response.stats.conflicts);
}

Properties

result

result: "unsatisfiable"

Defined in: src/types/sat.ts:151

Discriminant: the formula is unsatisfiable.

stats

stats: SatSolverStatsDto

Defined in: src/types/sat.ts:153

Solver statistics for this solve.