Type Alias: SatSolveResponse

@kortexya/reasoninglayer

---

@kortexya/reasoninglayer / Sat / SatSolveResponse

Type Alias: SatSolveResponse

SatSolveResponse = SatSatisfiableResult | SatUnsatisfiableResult | SatUnknownResult

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

Response from solving a propositional CNF formula.

Remarks

A discriminated union over SatVerdict: narrow on result to reach the model. stats is present in every branch.

Example

const response = await client.sat.solve({ numVars: 1, clauses: [[{ var: 0, negated: false }]] });
switch (response.result) {
  case 'satisfiable':
    console.log(response.model);
    break;
  case 'unsatisfiable':
    console.log('UNSAT');
    break;
  case 'unknown':
    console.log('budget exhausted');
    break;
}