Advanced simplifies the given formula by performing the following steps 1.

AdvancedWithHandler simplifies the given formula by performing the following steps 1.

CNFSubsumption performs subsumption on a given CNF formula and returns a new CNF.

DefaultConfig returns the default configuration for an advanced simplifier configuration.

The DefaultRatingFunction rates a formula by its string length.

Distribute simplifies the given formula by applying the distributive laws.

DNFSubsumption performs subsumption on a given DNF formula and returns a new DNF.

FactorOut simplifies a formula by applying factor out operations.

MinimizeNegations minimizes the number of negations of the given formula by applying De Morgan's Law heuristically for a smaller formula.

PropagateBackbone simplifies the given formula by computing its backbone and propagating it through the formula.

PropagateUnits performs unit propagation on the given formula.

QMC computes a simplification on the formula based on the algorithm by Quine and McCluskey.

QMCWithHandler computes a simplification on the formula based on the algorithm by Quine and McCluskey.

Config describes the configuration of an advanced simplifier.

A RatingFunction is used during simplification to compute the simplicity rating of a formula.