Skip to content

Interface: VariableFeasibilityDto

@kortexya/reasoninglayer


@kortexya/reasoninglayer / Spaces / VariableFeasibilityDto

Interface: VariableFeasibilityDto

Defined in: src/types/spaces.ts:184

Reachability of a single binary choice-point variable.

Remarks

Produced by mode = "feasibility" search.

  • canBeTrue = true means the solver actually observed a valid assignment with this variable = 1 (a witnessed model).
  • canBeFalse = true means the solver observed a valid assignment with this variable = 0.
  • canBeTrue = false && canBeFalse = false means the problem is UNSAT.

When the underlying solver hits a conflict/time budget before the opposite polarity could be proven (im)feasible, verified is false and the reachability fields reflect only the polarities that were actually witnessed. For example, (canBeTrue: true, canBeFalse: false, verified: false) means “observed in every model found so far, never observed as 0 — likely required, but the solver did not complete the UNSAT-for-0 probe to certify it.”

Properties

canBeFalse

canBeFalse: boolean

Defined in: src/types/spaces.ts:188

True if the solver witnessed a valid assignment where this variable is 0.


canBeTrue

canBeTrue: boolean

Defined in: src/types/spaces.ts:186

True if the solver witnessed a valid assignment where this variable is 1.


verified

verified: boolean

Defined in: src/types/spaces.ts:194

True when the reachability result is fully determined by the solver (both polarities resolved). False when a conflict/time limit was hit and the result reflects only the polarities that were observed.