Class FormulaAnalysis
- Namespace
- LogicalOptimizer
- Assembly
- LogicalOptimizer.dll
Semantic queries over a formula, built on the incremental SAT solver: backbone (literals forced in every model), projected model counting and enumeration, and backbone-based simplification. All queries work at any scale — no 2^n enumeration is involved.
public static class FormulaAnalysis- Inheritance
-
FormulaAnalysis
- Inherited Members
Methods
ComputeBackbone(AstNode, int, CancellationToken)
Compute the backbone: variables that take the same value in every model. Uses one SAT call per surviving candidate (incremental, with unsat-core-free filtering by counter-models).
public static BackboneResult ComputeBackbone(AstNode formula, int maxConflicts = 200000, CancellationToken cancellationToken = default)Parameters
formulaAstNodemaxConflictsintcancellationTokenCancellationToken
Returns
CountProjectedModels(AstNode, IReadOnlyCollection<string>, ResourceBudget?, CancellationToken)
Count the number of DISTINCT assignments over projectedVariables
(the projection scope P) that extend to some model of the formula; the
remaining variables are existentially forgotten. Sound against the overcount trap:
different full models that agree on P are counted once.
Scope semantics: projectedVariables MAY include names not
occurring in the formula — each such free variable multiplies the count by 2 and
is never an error. An empty projection returns 1 for a satisfiable formula
and 0 for an unsatisfiable one; projecting onto all of the formula's
variables equals CountModels().
Engine: SAT blocking enumeration — one incremental solve per distinct projected
model, blocking over the projection literals only (output-sensitive). The shared
ResourceBudget maps to two honest bounds: the number of enumerated
projected models (CoverStepLimit) and the SAT
conflicts allowed per solve (SatConflictLimit).
Exhausting either yields BudgetExhausted with
a null Count — a partial run is NEVER reported as exact. A null budget is
unbounded, subject only to cancellationToken, which throws
OperationCanceledException when signalled.
public static ProjectedModelCountResult CountProjectedModels(AstNode formula, IReadOnlyCollection<string> projectedVariables, ResourceBudget? budget = null, CancellationToken cancellationToken = default)Parameters
formulaAstNodeprojectedVariablesIReadOnlyCollection<string>budgetResourceBudgetcancellationTokenCancellationToken
Returns
EnumerateModels(AstNode, int, int, CancellationToken)
Enumerate models projected onto the input variables (each assignment appears
once; Tseitin auxiliaries are functionally determined). Lazily yields up to
maxModels models via incremental solving with blocking clauses.
public static IEnumerable<IReadOnlyDictionary<string, bool>> EnumerateModels(AstNode formula, int maxModels = 1000000, int maxConflicts = 200000, CancellationToken cancellationToken = default)Parameters
formulaAstNodemaxModelsintmaxConflictsintcancellationTokenCancellationToken
Returns
SimplifyWithBackbone(AstNode, int, CancellationToken)
Backbone-based simplification: forced variables become constants, then constant folding runs. Most useful beyond the exact-minimization range, where the rewrite pipeline has no truth-table support. Returns the input when nothing is forced or the backbone query exhausted its budget; an unsatisfiable formula becomes 0.
public static AstNode SimplifyWithBackbone(AstNode formula, int maxConflicts = 200000, CancellationToken cancellationToken = default)Parameters
formulaAstNodemaxConflictsintcancellationTokenCancellationToken