Interface: SatSolveRequest

@kortexya/reasoninglayer / Sat / SatSolveRequest

Interface: SatSolveRequest

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

Request body for solving a propositional CNF formula.

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

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

Properties

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?

optional maxConflicts: number

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

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

numVars

numVars: number

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

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

proofLogging?

optional proofLogging: boolean

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

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