simplification

Documentation

Overview

Package simplification gathers various simplification algorithms for Boolean formulas in LogicNG.

The idea of the simplifiers is to simplify a given formula. But what is "simple" in terms of a formula? Since "simple" is no mathematically defined term and can alter from application to application, some simplifiers let the user provide their own definition of "simple". This is done via a rating function.

A rating function is an interface which can be implemented by the user and computes a simplicity rating for a given formula. This could be for example the length of its string representation or the number of atoms. This rating function is then used to compare two formulas during the simplification process and thus deciding which of the formulas is the "simpler" one. There is a default rating function which is a rating function which compares formulas based on the length of their string representation (using the default string representation).

Implemented simplifications are - propagating its backbone - propagating its unit literals - applying the distributive law - factoring out common parts of the formula - minimize negations - subsumption on CNF and DNF formulas - an advanced simplification combining various methods including minimal prime implicant covers - a Quine-McCluskey implementation based on the advanced simplifier

To simplify a formula withe the advanced simplifier, you can simply call

simplified := simplification.Advanced(fac, formula)

Index

• func Advanced(fac f.Factory, formula f.Formula, config ...*Config) f.Formula
• func AdvancedWithHandler(fac f.Factory, formula f.Formula, optimizationHandler sat.OptimizationHandler, ...) (f.Formula, bool)
• func CNFSubsumption(fac f.Factory, formula f.Formula) (f.Formula, error)
• func DNFSubsumption(fac f.Factory, formula f.Formula) (f.Formula, error)
• func DefaultRatingFunction(fac f.Factory, formula f.Formula) float64
• func Distribute(fac f.Factory, formula f.Formula) f.Formula
• func FactorOut(fac f.Factory, formula f.Formula, ratingFunction ...RatingFunction) f.Formula
• func MinimizeNegations(fac f.Factory, formula f.Formula) f.Formula
• func PropagateBackbone(fac f.Factory, formula f.Formula) f.Formula
• func PropagateUnits(fac f.Factory, formula f.Formula) f.Formula
• func QMC(fac f.Factory, formula f.Formula) f.Formula
• func QMCWithHandler(fac f.Factory, formula f.Formula, optimizationHandler sat.OptimizationHandler) (f.Formula, bool)
• type Config
  • func DefaultConfig() *Config
  • func (Config) DefaultConfig() configuration.Config
  • func (Config) Sort() configuration.Sort
• type RatingFunction

Functions

func Advanced

func Advanced(fac f.Factory, formula f.Formula, config ...*Config) f.Formula

Advanced simplifies the given formula by performing the following steps

1. Computation of all prime implicants
2. Finding the minimal coverage over the found prime implicants (by finding one smallest MUS)
3. Building a DNF from the minimal prime implicant coverage
4. Factoring out common factors of the DNF using the FactorOut function
5. Minimizing negations of the factored-out DNF using the SimplifyNegations function

It can be configured with an optional advanced simplifier configuration.

func AdvancedWithHandler

func AdvancedWithHandler(
	fac f.Factory,
	formula f.Formula,
	optimizationHandler sat.OptimizationHandler,
	config ...*Config,
) (f.Formula, bool)

AdvancedWithHandler simplifies the given formula by performing the following steps

1. Computation of all prime implicants
2. Finding the minimal coverage over the found prime implicants (by finding one smallest MUS)
3. Building a DNF from the minimal prime implicant coverage
4. Factoring out common factors of the DNF using the FactorOut function
5. Minimizing negations of the factored-out DNF using the SimplifyNegations function

It can be configured with an optional advanced simplifier configuration. The given optimization handler can be used to abort the optimization function during the prime implicant computation.

func CNFSubsumption

func CNFSubsumption(fac f.Factory, formula f.Formula) (f.Formula, error)

CNFSubsumption performs subsumption on a given CNF formula and returns a new CNF. I.e. it performs as many subsumptions as possible. A subsumption in a CNF means, that e.g. a clause A | B | C is subsumed by another clause A | B and can therefore be deleted for an equivalent CNF. Returns with an error if the input formula was not in CNF.

func DNFSubsumption

func DNFSubsumption(fac f.Factory, formula f.Formula) (f.Formula, error)

DNFSubsumption performs subsumption on a given DNF formula and returns a new DNF. I.e. it performs as many subsumptions as possible. A subsumption in a DNF means, that e.g. a minterm A & B is subsumed by another clause A & B & C and can therefore be deleted for an equivalent DNF. Returns with an error if the input formula was not in DNF.

func DefaultRatingFunction

func DefaultRatingFunction(fac f.Factory, formula f.Formula) float64

The DefaultRatingFunction rates a formula by its string length.

func Distribute

func Distribute(fac f.Factory, formula f.Formula) f.Formula

Distribute simplifies the given formula by applying the distributive laws. In contrast to the FactorOut function, the distribution step is only performed once. E.g. for a formula (A | B) & (A | C & E) | B & C & D the Distribute function yields A | B & C & E | B & C & D whereas the FactorOut function also factors our B & C, yielding A | C & B & (E | D).

func FactorOut

func FactorOut(fac f.Factory, formula f.Formula, ratingFunction ...RatingFunction) f.Formula

FactorOut simplifies a formula by applying factor out operations. For example, given the formula A & B & C | A & D, both conjunction terms have the common factor A. Thus, the method returns A & (B & C | D). The optional ratingFunction can be used to rate functions between simplification steps and choose the one with the lower rating.

func MinimizeNegations

func MinimizeNegations(fac f.Factory, formula f.Formula) f.Formula

MinimizeNegations minimizes the number of negations of the given formula by applying De Morgan's Law heuristically for a smaller formula. The resulting formula is minimized for the length of its string representation (using the string representation which is defined in the formula's formula factory). For example, the formula ~A & ~B & ~C stays this way (since ~(A | B | C) is of same length as the initial formula), but the formula ~A & ~B & ~C & ~D is being transformed to ~(A | B | C | D) since its length is 16 vs. 17 in the un-simplified version.

func PropagateBackbone

func PropagateBackbone(fac f.Factory, formula f.Formula) f.Formula

PropagateBackbone simplifies the given formula by computing its backbone and propagating it through the formula. E.g. in the formula A & B & (A | B | C) & (~B | D) the backbone A, B is computed and propagated, yielding the simplified formula A & B & D.

func PropagateUnits

func PropagateUnits(fac f.Factory, formula f.Formula) f.Formula

PropagateUnits performs unit propagation on the given formula. Unit propagation works the following way: If a formula is such that a literal is forced for the formula to be satisfied, then this literal is propagated through the formula and thus simplifies the formula. For example, consider the formula (A | C) & ~C & (B | C) & (A | ~C) then the literal ~C is forced in the formula. Thus, the simplified formula (created by unit propagation) yields ~C & A & B.

func QMC

func QMC(fac f.Factory, formula f.Formula) f.Formula

QMC computes a simplification on the formula based on the algorithm by Quine and McCluskey. This implementation is however not based on the traditional term tables but uses a SAT solver based implementation based on the advanced simplifier. The resulting formula is in DNF.

func QMCWithHandler

func QMCWithHandler(
	fac f.Factory, formula f.Formula, optimizationHandler sat.OptimizationHandler,
) (f.Formula, bool)

QMCWithHandler computes a simplification on the formula based on the algorithm by Quine and McCluskey. This implementation is however not based on the traditional term tables but uses a SAT solver based implementation based on the advanced simplifier. The resulting formula is in DNF. The given optimization handler can be used to abort the optimization function during the prime implicant computation.

Types

type Config

type Config struct {
	FactorOut         bool
	RestrictBackbone  bool
	SimplifyNegations bool
	UseRatingFunction bool
	RatingFunction    RatingFunction
}

Config describes the configuration of an advanced simplifier. It holds flags for activating different simplification steps as well as an optional rating function.

func DefaultConfig

func DefaultConfig() *Config

DefaultConfig returns the default configuration for an advanced simplifier configuration.

func (Config) DefaultConfig

func (Config) DefaultConfig() configuration.Config

DefaultConfig returns the default configuration for an advanced simplifier configuration.

func (Config) Sort

func (Config) Sort() configuration.Sort

Sort returns the configuration sort (Advanced Simplifier).

type RatingFunction

type RatingFunction func(fac f.Factory, formula f.Formula) float64

A RatingFunction is used during simplification to compute the simplicity rating of a formula. This rating is then used to compare it during simplification and choosing the formula with the lowest rating.