Interface: ProofExportRequest

@kortexya/reasoninglayer

---

@kortexya/reasoninglayer / ProofEngine / ProofExportRequest

Interface: ProofExportRequest

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

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

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

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

Properties

clauses

clauses: ProofLiteralDto[][]

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

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

---

format

format: ProofExportFormat

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

Target certificate format.

---

maxConflicts?

optional maxConflicts: number

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

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

Default Value

1000000

---

numVars

numVars: number

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

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