normalform

package
v0.4.0 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: May 11, 2024 License: MIT Imports: 7 Imported by: 1

Documentation

Overview

Package normalform provides algorithms for converting Boolean formulas into normal forms in LogicNG.

The two most important normal forms are the conjunctive normal form (CNF) and the disjunctive normal form (DNF). In particular, the CNF is of special importance, since it is the input form required for SAT Solving and many other operations or algorithms.

Another important normal form is the negation normal form (NNF) where only the operators ~, &, and | are allowed and negations must only appear before variables. In LogicNG this means that the formula consists only of literals Ands, and Ors. The NNF is often used as pre-processing step before transforming the formula into another normal form. Also, some algorithms require a formula to be in NNF to work.

Simple normal-forms can be computed like this: 

normalform.NNF(fac, formula)               // negation normal form
normalform.TseitinCNFDefault(fac, formula) // CNF due to Tseitin
normalform.PGCNFDefault(fac, formula)      // CNF due to Plaisted & Greenbaum
normalform.FactorizedCNF(fac, formula)     // CNF by factorization
normalform.FactorizedDNF(fac, formula)     // DNF by factorization

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func AIG 

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

AIG returns the given formula as AIG (and-inverter-graph), therefore only containing conjunctions and negations.

func CNF 

func CNF(fac f.Factory, formula f.Formula, config ...*CNFConfig) f.Formula

CNF returns a conjunctive normal form of the given formula with the optional CNF configuration. If no configuration is provided, the advanced CNF algorithm is used. This algorithm encodes the given formula to CNF by first trying to use factorization for the single sub-formulas. When certain user-provided boundaries are met, the method is switched to Tseitin or Plaisted & Greenbaum as a fallback.

func FactorizedCNF 

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

FactorizedCNF returns the given formula in conjunctive normal form. The algorithm used is factorization. The resulting CNF can grow exponentially, therefore unless you are sure that the input is sensible, prefer the CNF factorization with a handler in order to be able to abort it.

func FactorizedCNFWithHandler 

func FactorizedCNFWithHandler(
	fac f.Factory, formula f.Formula, factorizatonHandler FactorizationHandler,
) (cnf f.Formula, ok bool)

FactorizedCNFWithHandler returns the given formula in conjunctive normal form. The given handler can be used to abort the factorization. Returns the CNF and an ok flag which is false when the handler aborted the computation.

func FactorizedDNF 

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

FactorizedDNF returns the given formula in disjunctive normal form. A DNF is a disjunction of conjunctions of literals. The algorithm used is factorization. The resulting DNF can grow exponentially, therefore unless you are sure that the input is sensible, prefer the DNF factorization with a handler in order to be able to abort it.

func FactorizedDNFWithHandler 

func FactorizedDNFWithHandler(
	fac f.Factory, formula f.Formula, factorizationHandler FactorizationHandler,
) (dnf f.Formula, ok bool)

FactorizedDNFWithHandler returns the given formula in disjunctive normal form. A DNF is a disjunction of conjunctions of literals. The given handler can be used to abort the factorization. Returns the DNF and an ok flag which is false when the handler aborted the computation.

func IsAIG 

func IsAIG(fac f.Factory, formula f.Formula) bool

IsAIG reports whether the given formula is in AIG (and-inverter-graph) normal-form, therefore only containing conjunctions and negations.

func IsCNF 

func IsCNF(fac f.Factory, formula f.Formula) bool

IsCNF reports whether the given formula is in conjunctive normal form. A CNF is a conjunction of discjuntion of literals.

func IsDNF 

func IsDNF(fac f.Factory, formula f.Formula) bool

IsDNF reports whether the given formula is in disjunctive normal form. A DNF is a disjunction of conjunctions of literals.

func IsMaxterm 

func IsMaxterm(fac f.Factory, formula f.Formula) bool

IsMaxterm reports whether the given formula is a maxterm, i.e. a disjunction of literals.

func IsMinterm 

func IsMinterm(fac f.Factory, formula f.Formula) bool

IsMinterm reports whether the given formula is a minterm, i.e. a conjunction of literals.

func IsNNF 

func IsNNF(fac f.Factory, formula f.Formula) bool

IsNNF reports whether the given formula is in negation normal form. In an NNF only negation, conjunction, and disjunction are allowed and negations must only appear before variables.

func NNF 

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

NNF returns the negation normal form of the given formula. In an NNF only negation, conjunction, and disjunction are allowed and negations must only appear before variables.

func PGCNF 

func PGCNF(fac f.Factory, formula f.Formula, boundaryForFactorization int, state *CNFAuxState) f.Formula

PGCNF transforms a formula to CNF with the algorithm by Plaisted & Greenbaum. Depending on the polarity of a sub-formula of the formula's parse tree it is replaced by a new auxiliary variable and an implication between variable and sub-formula is added. The given boundaryForFactorization determines up to which number of atoms sub-formulas are transformed by factorization instead of the PG algorithm. The state which stores introduced auxiliary variables is provided by the caller and can therefore be reused between different executions of the method.

func PGCNFDefault 

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

PGCNFDefault transforms a formula to CNF with the algorithm by Plaisted & Greenbaum. Depending on the polarity of a sub-formula of the formula's parse tree it is replaced by a new auxiliary variable and an implication between variable and sub-formula is added. In this default variant of the transformation sub-formulas with less than 12 atoms are transformed by factorization and auxiliary variables are only reused within one execution of the algorithm

func PGCNFWithBoundary 

func PGCNFWithBoundary(fac f.Factory, formula f.Formula, boundaryForFactorization int) f.Formula

PGCNFWithBoundary transforms a formula to CNF with the algorithm by Plaisted & Greenbaum. Depending on the polarity of a sub-formula of the formula's parse tree it is replaced by a new auxiliary variable and an implication between variable and sub-formula is added. The given boundaryForFactorization determines up to which number of atoms sub-formulas are transformed by factorization instead of the PG algorithm. Auxiliary variables are only reused within one execution of the algorithm.

func TseitinCNF 

func TseitinCNF(fac f.Factory, formula f.Formula, boundaryForFactorization int, state *CNFAuxState) f.Formula

TseitinCNF transforms a formula to CNF with the algorithm by Tseitin. Each sub-formula of the formula's parse tree is replaced by a new auxiliary variable and an equivalence between the new variable and the sub-formula is added. The given boundaryForFactorization determines up to which number of atoms sub-formulas are transformed by factorization instead of the Tseitin algorithm. The state which stores introduced auxiliary variables is provided by the caller and can therefore be reused between different executions of the method.

func TseitinCNFDefault 

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

TseitinCNFDefault transforms a formula to CNF with the algorithm by Tseitin. Each sub-formula of the formula's parse tree is replaced by a new auxiliary variable and an equivalence between the new variable and the sub-formula is added. In this default variant of the transformation sub-formulas with less than 12 atoms are transformed by factorization and auxiliary variables are only reused within one execution of the algorithm

func TseitinCNFWithBoundary 

func TseitinCNFWithBoundary(fac f.Factory, formula f.Formula, boundaryForFactorization int) f.Formula

TseitinCNFWithBoundary transforms a formula to CNF with the algorithm by Tseitin. Each sub-formula of the formula's parse tree is replaced by a new auxiliary variable and an equivalence between the new variable and the sub-formula is added. The given boundaryForFactorization determines up to which number of atoms sub-formulas are transformed by factorization instead of the Tseitin algorithm. Auxiliary variables are only reused within one execution of the algorithm.

Types

type CNFAlgorithm 

type CNFAlgorithm byte

CNFAlgorithm encodes the different algorithms for converting a formula to CNF. 

const (
	CNFFactorization CNFAlgorithm = iota
	CNFTseitin
	CNFPlaistedGreenbaum
	CNFAdvanced
)

func (CNFAlgorithm) String 

func (i CNFAlgorithm) String() string

type CNFAuxState 

type CNFAuxState struct {
	FormulaMap map[f.Formula]f.Formula
	LiteralMap map[f.Formula]f.Literal
}

CNFAuxState is holds the variable and formula mapping for a Tseitin or Plaisted & Greenbaum CNF transformation. If you want to reuse generated CNF auxiliary variables you can re-use such a state between different CNF computations.

func NewCNFAuxState 

func NewCNFAuxState() *CNFAuxState

NewCNFAuxState generates a new empty state for Tseitin or Plaisted & Greenbaum CNF transformations.

type CNFConfig 

type CNFConfig struct {
	Algorithm                            CNFAlgorithm
	FallbackAlgorithmForAdvancedEncoding CNFAlgorithm
	DistributionBoundary                 int
	CreatedClauseBoundary                int
	AtomBoundary                         int
}

CNFConfig represents the configuration for the CNF conversion. It stores the main algorithm to transform the formula. If the advanced algorithm is chosen, also a fallback algorithm has to be chosen. Furthermore boundaries for number of distributions, created clauses, or atoms can be provided for the advanced algorithm.

func DefaultCNFConfig 

func DefaultCNFConfig() *CNFConfig

DefaultCNFConfig returns the default configuration for a CNF configuration.

func (CNFConfig) DefaultConfig 

func (CNFConfig) DefaultConfig() configuration.Config

DefaultConfig returns the default configuration for a CNF configuration.

func (CNFConfig) Sort 

func (CNFConfig) Sort() configuration.Sort

Sort returns the configuration sort (CNF).

type CNFHandler 

type CNFHandler struct {
	// contains filtered or unexported fields
}

CNFHandler is a special handler for the advanced CNF algorithm.

func NewCNFHandler 

func NewCNFHandler(distributionBoundary, clauseBoundary int) *CNFHandler

NewCNFHandler returns a new handler for the advanced CNF transformation with the given distribution and clause boundary.

func (*CNFHandler) Aborted 

func (h *CNFHandler) Aborted() bool

Aborted reports whether the handler was aborted.

func (*CNFHandler) CreatedClause 

func (h *CNFHandler) CreatedClause(clause f.Formula) bool

CreatedClause is called each time a clause is created during the factorization and returns true if the computation should be continued.

func (*CNFHandler) PerformedDistribution 

func (h *CNFHandler) PerformedDistribution() bool

PerformedDistribution is called each time a distribution during the factorization is performed and returns true if the computation should be continued.

func (*CNFHandler) Started 

func (h *CNFHandler) Started()

Started is called when the CNF factorization starts.

type FactorizationHandler 

type FactorizationHandler interface {
	handler.Handler
	PerformedDistribution() bool
	CreatedClause(clause f.Formula) bool
}

FactorizationHandler is a special handler able to abort CNF or DNF factorizations.

type TimeoutHandler added in v0.4.0 

type TimeoutHandler struct {
	handler.Timeout
}

A TimeoutHandler can be used to abort a CNF factorization depending on a timeout set beforehand.

func HandlerWithTimeout added in v0.4.0 

func HandlerWithTimeout(timeout handler.Timeout) *TimeoutHandler

HandlerWithTimeout generates a new timeout handler with the given timeout.

func (*TimeoutHandler) CreatedClause added in v0.4.0 

func (h *TimeoutHandler) CreatedClause(clause f.Formula) bool

CreatedClause is called each time a clause is created during the factorization and returns true if the computation should be continued.

func (*TimeoutHandler) PerformedDistribution added in v0.4.0 

func (h *TimeoutHandler) PerformedDistribution() bool

PerformedDistribution is called each time a distribution during the factorization is performed and returns true if the computation should be continued.

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.