Class ExternalSatEquivalenceChecker

Namespace: LogicalOptimizer

Assembly: LogicalOptimizer.dll

Equivalence backend that routes the SAT-miter query through a user-supplied IExternalSatSolver (e.g. a process adapter around CaDiCaL or Kissat) while everything else — miter construction, Tseitin encoding, counterexample decoding — stays in-library. Opt-in only: the default backends remain HybridEquivalenceChecker and BddEquivalenceChecker on the embedded engines.

Trust model: a Satisfiable verdict (non-equivalence) is VERIFIED — the returned model must satisfy the miter CNF (checked in linear time via IsSatisfiedBy(IReadOnlyList<int>)), otherwise the solver is lying or broken and an InvalidOperationException is thrown. An Unsatisfiable verdict (equivalence) is TRUSTED — refuting it cheaply is not possible; demand a DRAT/LRAT proof from the solver and check it out of band if the equivalence claim must be independently verifiable.

public sealed class ExternalSatEquivalenceChecker : IEquivalenceChecker

Inheritance: object

ExternalSatEquivalenceChecker

Implements: IEquivalenceChecker

Inherited Members: object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.ReferenceEquals(object, object)

object.ToString()

Constructors

ExternalSatEquivalenceChecker(IExternalSatSolver)

Create a checker that sends every miter query to solver.

public ExternalSatEquivalenceChecker(IExternalSatSolver solver)

Parameters

solver IExternalSatSolver

Methods

Check(AstNode, AstNode, CancellationToken)

Check equivalence through the external solver: UNSAT miter means equivalent (trusted), SAT yields a verified counterexample over the input variables, Unknown passes through as an inconclusive verdict.

public EquivalenceCheckResult Check(AstNode left, AstNode right, CancellationToken cancellationToken = default)

Parameters

left AstNode
right AstNode
cancellationToken CancellationToken

Returns

EquivalenceCheckResult