Skip to content
KortexyaKortexyaReasoning Layer SDK

Interface: SatSolveRequest

@kortexya/reasoninglayer

@kortexya/reasoninglayer / SatSolveRequest

Interface: SatSolveRequest

Section titled “Interface: SatSolveRequest”

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

Request body for solving a propositional CNF formula.

Remarks

Section titled “Remarks”

The formula is the conjunction of clauses; each clause is a non-empty disjunction of SatLiteralDtos. No tenant context is required — the solver is stateless.

Example

Section titled “Example”
// (x0 ∨ ¬x1) ∧ (x1)
const request: SatSolveRequest = {
  numVars: 2,
  clauses: [
    [{ var: 0, negated: false }, { var: 1, negated: true }],
    [{ var: 1, negated: false }],
  ],
};

Properties

Section titled “Properties”

clauses

Section titled “clauses”

clauses: SatLiteralDto[][]

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

CNF clauses. Each clause is a non-empty list of literals. The formula is the conjunction of all clauses.

maxConflicts?

Section titled “maxConflicts?”

optional maxConflicts?: number

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

Maximum number of conflicts before returning "unknown". 0 means unlimited (default).

numVars

Section titled “numVars”

numVars: number

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

Total number of propositional variables (variables are 0 .. numVars-1).

proofLogging?

Section titled “proofLogging?”

optional proofLogging?: boolean

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

Whether to enable DRAT proof logging (expensive; disabled by default).