Skip to content
KortexyaKortexyaReasoning Layer SDK

Interface: ProofExportRequest

@kortexya/reasoninglayer

@kortexya/reasoninglayer / ProofExportRequest

Interface: ProofExportRequest

Section titled “Interface: ProofExportRequest”

Defined in: src/types/proof-engine.ts:535

Request to prove a CNF unsatisfiable and export the refutation certificate.

Remarks

Section titled “Remarks”

The CNF is a conjunction of clauses, each a disjunction of literals. No tenant context is involved — the solver is stateless and in-process.

Example

Section titled “Example”
// (x0) ∧ (¬x0) — immediately unsatisfiable
const request: ProofExportRequest = {
  numVars: 1,
  clauses: [[{ var: 0 }], [{ var: 0, negated: true }]],
  format: 'drat',
};

Properties

Section titled “Properties”

clauses

Section titled “clauses”

clauses: ProofLiteralDto[][]

Defined in: src/types/proof-engine.ts:539

The CNF: a conjunction of clauses, each a disjunction of literals.

format

Section titled “format”

format: ProofExportFormat

Defined in: src/types/proof-engine.ts:541

Target certificate format.

maxConflicts?

Section titled “maxConflicts?”

optional maxConflicts?: number

Defined in: src/types/proof-engine.ts:546

Conflict budget before the solver gives up (and returns unknown).

Default Value

Section titled “Default Value”
1000000

numVars

Section titled “numVars”

numVars: number

Defined in: src/types/proof-engine.ts:537

Number of propositional variables (variable indices are 0..numVars).