Class EquivalenceChecker

Namespace

LogicalOptimizer

Assembly

LogicalOptimizer.dll

Equivalence of two boolean expressions at any scale. Small expressions are compared by truth table; larger ones through a miter (XOR of both sides) put through the Tseitin transformation and the built-in SAT solver — UNSAT proves equivalence without enumerating 2^n rows, SAT yields a concrete counterexample.

public static class EquivalenceChecker

Inheritance

object

EquivalenceChecker

Inherited Members

object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.MemberwiseClone()

object.ReferenceEquals(object, object)

object.ToString()

Fields

DefaultMaxConflicts

Default conflict budget for one SAT-based equivalence query.

public const int DefaultMaxConflicts = 200000

Field Value

int

Methods

Check(AstNode, AstNode, int, CancellationToken)

public static EquivalenceCheckResult Check(AstNode left, AstNode right, int maxConflicts = 200000, CancellationToken cancellationToken = default)

Parameters

left AstNode

right AstNode

maxConflicts int

cancellationToken CancellationToken

Returns

EquivalenceCheckResult

Check(string, string, int, CancellationToken)

public static EquivalenceCheckResult Check(string left, string right, int maxConflicts = 200000, CancellationToken cancellationToken = default)

Parameters

left string

right string

maxConflicts int

cancellationToken CancellationToken

Returns

EquivalenceCheckResult

CheckWithProof(AstNode, AstNode, int, CancellationToken)

SAT-miter equivalence that also returns a DRAT proof when the verdict is "equivalent" (UNSAT of the miter). The proof is checkable against the miter's Tseitin CNF (also returned) by any DRAT/RUP checker, e.g. drat-trim — the equivalence claim becomes externally verifiable rather than trusted.

public static (EquivalenceCheckResult Result, TseitinCnf MiterCnf, string? DratProof) CheckWithProof(AstNode left, AstNode right, int maxConflicts = 200000, CancellationToken cancellationToken = default)

Parameters

left AstNode

right AstNode

maxConflicts int

cancellationToken CancellationToken

Returns

(EquivalenceCheckResult Result, TseitinCnf MiterCnf, string DratProof)