Interface: SatSatisfiableResult

@kortexya/reasoninglayer

---

@kortexya/reasoninglayer / Sat / SatSatisfiableResult

Interface: SatSatisfiableResult

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

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

Remarks

model holds the Boolean assignment for every variable, indexed by variable number (model[0] is the value of variable 0). Its length is SatSolveRequest.numVars.

Example

if (response.result === 'satisfiable') {
  console.log(response.model[0]); // value assigned to x0
}

Properties

model

model: boolean[]

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

Boolean assignment for each variable (index 0 = variable 0).

---

result

result: "satisfiable"

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

Discriminant: the formula is satisfiable.

---

stats

stats: SatSolverStatsDto

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

Solver statistics for this solve.