Interface IExternalSatSolver
- Namespace
- LogicalOptimizer
- Assembly
- LogicalOptimizer.Sat.dll
Seam for plugging an external SAT solver (CaDiCaL, Kissat, a solver behind a service, ...) into consumers that otherwise use the embedded CDCL solver. The contract is deliberately minimal and one-shot — CNF in, verdict out — not an incremental IPASIR binding: the library keeps parsing, Tseitin encoding and counterexample decoding, and only the raw CNF query is handed off.
Trust model (asymmetric, enforced by the in-library consumers such as
ExternalSatEquivalenceChecker): a Satisfiable
verdict must come with a model, and the model IS verified against the CNF
(cheap, linear in the clause count) — a bogus model is detected and rejected.
A Unsatisfiable verdict cannot be checked cheaply and
is TRUSTED; if that matters, run a proof-producing solver and check its
DRAT/LRAT certificate out of band (e.g. with drat-trim).
public interface IExternalSatSolverMethods
Solve(ExternalSatProblem, CancellationToken)
Decide satisfiability of problem. Implementations should
honor cancellationToken (throw
OperationCanceledException) and report
Unknown when they give up without a verdict
(timeout, resource limit, solver not available mid-flight).
ExternalSatResult Solve(ExternalSatProblem problem, CancellationToken cancellationToken = default)Parameters
problemExternalSatProblemcancellationTokenCancellationToken