bdd

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: 16 Imported by: 1

Documentation

Overview

Package bdd provides data structures and algorithms on Binary Decision Diagrams (BDD) in LogicNG.

A BDD is a directed acyclic graph of a given formula. It has a single root; Each inner node is labeled with a propositional variable and has one outgoing edge for a positive assignment, and one edge for a negative assignment of the respective variable. The leaves are labeled with 1 and 0 representing true and false. An assignment is represented by a path from the root node to a leaf and its evaluation is the respective value of the leaf. Therefore, all paths to a 1-leaf are valid (possibly partial) models for the formula.

Crucial for a small BDD representation of a formula is a good variable ordering. There are different orderings implemented in LogicNG: based on variable occurrence, DFS- or BFS based, and the FORCE heuristic.

A BDD is always compiled by a kernel. This kernel holds all internal data structures used during the compilation, especially the node cache. Algorithms on BDDs always require the kernel which was used to compile the BDD.

The following example creates an BDD of a formula without configuring a specific kernel or variable ordering: 

fac := formula.NewFactory()
formula := fac.Or(fac.Variable("a"), fac.Variable("b")) // formula a / b
bdd := bdd.Build(fac, formula)

You can also configure the node table size and the cache size of the kernel by hand. The BDD kernel internally holds a table with all nodes in the BDD. This table can be extended dynamically, but this is an expensive operation. On the other hand, one wants to avoid reserving too much space for nodes, since this costs unnecessary memory. 30 * x proved to be efficient in practice for medium-sized formulas. The following example manually creates a kernel with a node table size of 10 and a cache size of 100. 

fac := formula.NewFactory()
formula := fac.Or(fac.Variable("a"), fac.Variable("b")) // formula a / b
kernel := bdd.NewKernel(fac, 2, 10, 100)
bdd := bdd.BuildWithKernel(fac, formula, kernel)

Finally, you can also compute a variable ordering first and create the BDD with the given ordering. 

fac := formula.NewFactory()
p := parser.NewPropositionalParser(fac)
formula := p.Parse("(A => ~B) & ((A & C) | (D & ~C)) & (A | Y | X) & (Y <=> (X | (W + A + F < 1)))")
ordering := bdd.DfsOrder(fac, formula)
kernel := bdd.NewKernelWithOrdering(fac, ordering, 10, 100)
bdd := bdd.BuildWithKernel(fac, formula, kernel)

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func BFSOrder 

func BFSOrder(fac f.Factory, formula f.Formula) []f.Variable

BFSOrder generates a breadth-first-search variable ordering for the given formula. It traverses the formula in a BFS manner and gathers all variables in the occurrence.

func CNF 

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

CNF transforms a given formula into a CNF by using a BDD. The resulting CNF does not contain any auxiliary variables, but can have quite a large size.

func CNFWithHandler added in v0.4.0 

func CNFWithHandler(fac f.Factory, formula f.Formula, bddHandler Handler) (cnf f.Formula, ok bool)

CNFWithHandler transforms a given formula into a CNF by using a BDD. The resulting CNF does not contain any auxiliary variables, but can have quite a large size. The bddHandler can be used to abort the BDD compilation. If the BDD compilation was aborted, the ok flag is false.

func DFSOrder 

func DFSOrder(fac f.Factory, formula f.Formula) []f.Variable

DFSOrder generates a depth-first-search variable ordering for the given formula. It traverses the formula in a DFS manner and gathers all variables in the occurrence.

func DNF 

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

DNF transforms a given formula into a DNF by using a BDD. The resulting DNF does not contain any auxiliary variables, but can have quite a large size.

func DNFWithHandler added in v0.4.0 

func DNFWithHandler(fac f.Factory, formula f.Formula, bddHandler Handler) (cnf f.Formula, ok bool)

DNFWithHandler transforms a given formula into a DNF by using a BDD. The resulting DNF does not contain any auxiliary variables, but can have quite a large size. The bddHandler can be used to abort the BDD compilation. If the BDD compilation was aborted, the ok flag is false.

func ForceOrder 

func ForceOrder(fac f.Factory, formula f.Formula) []f.Variable

ForceOrder generates a variable ordering for the given formula according to the FORCE ordering due to Aloul, Markov, and Sakallah. This ordering only works for CNF formulas. This method converts the formula to CNF before this ordering is called which can have side effects on the generated CNF variables and/or the formula caches in the factory.

func GenerateGraphical 

func GenerateGraphical(bdd *BDD, generator *GraphicalGenerator) *graphical.Representation

GenerateGraphical generates a graphical representation of the given bdd with the configuration of the generator. The resulting representation can then be exported as mermaid or graphviz graph.

func MaxToMinOrder 

func MaxToMinOrder(fac f.Factory, formula f.Formula) []f.Variable

MaxToMinOrder generates a variable ordering sorting the variables from maximal to minimal occurrence in the input formula. If two variables have the same number of occurrences, their ordering according to their DFS ordering will be considered.

func MinToMaxOrder 

func MinToMaxOrder(fac f.Factory, formula f.Formula) []f.Variable

MinToMaxOrder generates a variable ordering sorting the variables from minimal to maximal occurrence in the input formula. If two variables have the same number of occurrences, their ordering according to their DFS ordering will be considered.

Types

type BDD 

type BDD struct {
	Kernel *Kernel
	Index  int32
}

A BDD is a canonical representation of a Boolean formula. It contains a pointer to the kernel which was used to generate the BDD and the node index of the BDD within this kernel.

func Compile added in v0.3.0 

func Compile(fac f.Factory, formula f.Formula) *BDD

Compile creates a BDD for a given formula. The variable ordering in this case is the order in which the variables occur in the formula.

func CompileLiterals added in v0.3.0 

func CompileLiterals(literals []f.Literal, kernel *Kernel) *BDD

CompileLiterals creates a BDD for a conjunction of literals with a given kernel.

func CompileWithHandler added in v0.3.0 

func CompileWithHandler(fac f.Factory, formula f.Formula, bddHandler Handler) (bdd *BDD, ok bool)

CompileWithHandler creates a BDD for a given formula with the given bddHandler. The handler can abort the BDD creation based on the number of nodes created during the BDD compilation process. If the BDD compilation was aborted, the ok flag is false.

func CompileWithKernel added in v0.3.0 

func CompileWithKernel(fac f.Factory, formula f.Formula, kernel *Kernel) *BDD

CompileWithKernel creates a BDD for a given formula with a given kernel.

func CompileWithKernelAndHandler added in v0.3.0 

func CompileWithKernelAndHandler(
	fac f.Factory,
	formula f.Formula,
	kernel *Kernel,
	bddHandler Handler,
) (bdd *BDD, ok bool)

CompileWithKernelAndHandler creates a BDD for a given formula with a given kernel and bddHandler. The handler can abort the BDD creation based on the number of nodes created during the BDD compilation process. If the BDD compilation was aborted, the ok flag is false.

func CompileWithVarOrder added in v0.3.0 

func CompileWithVarOrder(fac f.Factory, formula f.Formula, order []f.Variable) *BDD

CompileWithVarOrder creates a BDD for a given formula and a variable ordering.

func CompileWithVarOrderAndHandler added in v0.3.0 

func CompileWithVarOrderAndHandler(
	fac f.Factory,
	formula f.Formula,
	order []f.Variable,
	bddHandler Handler,
) (bdd *BDD, ok bool)

CompileWithVarOrderAndHandler creates a BDD for a given formula, variable ordering, and bddHandler. The handler can abort the BDD creation based on the number of nodes created during the BDD compilation process. If the BDD compilation was aborted, the ok flag is false.

func (*BDD) And 

func (b *BDD) And(other *BDD) *BDD

And returns a newBdd BDD which is the conjunction of the BDD and the given other BDD. This method panics if the BDDs were constructed by different kernels.

func (*BDD) CNF 

func (b *BDD) CNF() f.Formula

CNF returns a CNF formula for the BDD.

func (*BDD) DNF 

func (b *BDD) DNF() f.Formula

DNF returns a DNF formula for the BDD.

func (*BDD) Equivalence 

func (b *BDD) Equivalence(other *BDD) *BDD

Equivalence returns a newBdd BDD which is the equivalence of the BDD and the other given BDD. This method panics if the BDDs were constructed by different kernels.

func (*BDD) Exists 

func (b *BDD) Exists(variable ...f.Variable) *BDD

Exists performs existential quantifier elimination for a given set of variables and return the resulting BDD.

func (*BDD) ForAll 

func (b *BDD) ForAll(variable ...f.Variable) *BDD

ForAll performs universal quantifier elimination for a given set of variables and returns the resulting BDD.

func (*BDD) FullModel 

func (b *BDD) FullModel() (*model.Model, error)

FullModel returns a model over all variables of the BDD. An error is returned if the BDD is a contradiction and therefore has no model.

func (*BDD) ImpliedBy 

func (b *BDD) ImpliedBy(other *BDD) *BDD

ImpliedBy returns a newBdd BDD which is the implication of the other given BDD to the BDD. This method panics if the BDDs were constructed by different kernels.

func (*BDD) Implies 

func (b *BDD) Implies(other *BDD) *BDD

Implies returns a newBdd BDD which is the implication of the BDD to the given other BDD. This method panics if the BDDs were constructed by different kernels.

func (*BDD) IsContradiction 

func (b *BDD) IsContradiction() bool

IsContradiction reports whether the BDD is a tautology.

func (*BDD) IsTautology 

func (b *BDD) IsTautology() bool

IsTautology reports whether the BDD is a tautology.

func (*BDD) Model 

func (b *BDD) Model() (*model.Model, error)

Model returns an arbitrary model of the BDD. An error is returned if the BDD is a contradiction and therefore has no model.

func (*BDD) ModelCount 

func (b *BDD) ModelCount() *big.Int

ModelCount returns the number of satisfying models of the BDD.

func (*BDD) ModelEnumeration 

func (b *BDD) ModelEnumeration(variables ...f.Variable) []*model.Model

ModelEnumeration enumerates all models of the BDD wrt. a given set of variables.

func (*BDD) ModelWithVariables 

func (b *BDD) ModelWithVariables(defaultValue bool, variable ...f.Variable) (*model.Model, error)

ModelWithVariables returns an arbitrary model of the BDD which contains at least the given variables. If a variable is a don't care variable, it will be assigned with the given defaultValue. An error is returned if the BDD is a contradiction and therefore has no model.

func (*BDD) Negate 

func (b *BDD) Negate() *BDD

Negate returns a newBdd BDD which is the negation of the BDD.

func (*BDD) NodeCount 

func (b *BDD) NodeCount() int

NodeCount returns the number of distinct nodes for the BDD.

func (*BDD) NodeRepresentation added in v0.4.0 

func (b *BDD) NodeRepresentation() Node

NodeRepresentation returns a graph-like representation of the BDD as nodes.

func (*BDD) NumberOfCNFClauses 

func (b *BDD) NumberOfCNFClauses() *big.Int

NumberOfCNFClauses returns the number of clauses for the CNF formula of the BDD.

func (*BDD) Or 

func (b *BDD) Or(other *BDD) *BDD

Or returns a newBdd BDD which is the disjunction of the BDD and the given other BDD. This method panics if the BDDs were constructed by different kernels.

func (*BDD) PathCountOne 

func (b *BDD) PathCountOne() *big.Int

PathCountOne returns the number of paths leading to the terminal 1 node.

func (*BDD) PathCountZero 

func (b *BDD) PathCountZero() *big.Int

PathCountZero returns the number of paths leading to the terminal 0 node.

func (*BDD) Restrict 

func (b *BDD) Restrict(restriction ...f.Literal) *BDD

Restrict returns a newBdd BDD where the literals of the restriction are assigned to their respective polarity and therefore the BDD does not contain the respective variables anymore.

func (*BDD) Support 

func (b *BDD) Support() []f.Variable

Support returns all the variables the BDD depends on.

func (*BDD) ToFormula 

func (b *BDD) ToFormula(fac f.Factory, followPathsToTrue ...bool) f.Formula

ToFormula returns a formula representation of the BDD. This is done by using the Shannon expansion. If followPathsToTrue is activated, the paths leading to the true terminal are followed to generate the formula. If followPathsToTrue is deactivated, the paths leading to the false terminal are followed to generate the formula and the resulting formula is negated. Depending on the formula and the number of satisfying assignments, the generated formula can be more compact using the true paths or false paths, respectively.

func (*BDD) VariableOrder 

func (b *BDD) VariableOrder() []f.Variable

VariableOrder returns the variable order of the BDD.

func (*BDD) VariableProfile 

func (b *BDD) VariableProfile() map[f.Variable]int

VariableProfile returns how often each variable occurs in the BDD.

type ConstantNode added in v0.4.0 

type ConstantNode struct {
	Value bool
}

ConstantNode represents a terminal node in a BDD.

func (ConstantNode) High added in v0.4.0 

func (c ConstantNode) High() Node

High returns the node of the high edge or nil for a terminal node.

func (ConstantNode) InnerNode added in v0.4.0 

func (c ConstantNode) InnerNode() bool

Reports whether the node is an inner node.

func (ConstantNode) Label added in v0.4.0 

func (c ConstantNode) Label() string

Label returns the label of the node. Can either be a variable or a constant.

func (ConstantNode) Low added in v0.4.0 

func (c ConstantNode) Low() Node

Low returns the node of the low edge or nil for a terminal node.

func (ConstantNode) String added in v0.4.0 

func (c ConstantNode) String() string

type GraphicalGenerator 

type GraphicalGenerator struct {
	*graphical.Generator[int32]
	DefaultNegativeEdgeStyle *graphical.EdgeStyle
	ComputeNegativeEdgeStyle func(src, dst int32) *graphical.EdgeStyle
}

A GraphicalGenerator is used to configure the graphical representation of a BDD as mermaid or Graphviz graphic. It inherits all fields of graphical.Generator. The graphical.Generator.DefaultEdgeStyle is used as the default edge style for the positive BDD edges. The DefaultNegativeEdgeStyle is specific to the BDD generator and is used for negative BDD edges. The same holds for graphical.Generator.ComputeEdgeStyle and ComputeNegativeEdgeStyle.

func DefaultGenerator 

func DefaultGenerator() *GraphicalGenerator

DefaultGenerator returns a BDD generator with sensible defaults. Positive edges are solid green lines whereas negative edges are dotted red lines.

type Handler 

type Handler interface {
	handler.Handler
	NewRefAdded() bool
}

A Handler for a BDD can abort the compilation of a BDD. The method NewRefAdded is called by the BDD compiler everytime a new BDD node reference is added.

type InnerNode added in v0.4.0 

type InnerNode struct {
	Variable string
	LowNode  Node
	HighNode Node
}

InnerNode represents an inner node in a BDD.

func (InnerNode) High added in v0.4.0 

func (n InnerNode) High() Node

High returns the node of the high edge or nil for a terminal node.

func (InnerNode) InnerNode added in v0.4.0 

func (n InnerNode) InnerNode() bool

Reports whether the node is an inner node.

func (InnerNode) Label added in v0.4.0 

func (n InnerNode) Label() string

Label returns the label of the node. Can either be a variable or a constant.

func (InnerNode) Low added in v0.4.0 

func (n InnerNode) Low() Node

Low returns the node of the low edge or nil for a terminal node.

func (InnerNode) String added in v0.4.0 

func (n InnerNode) String() string

type Kernel 

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

A Kernel holds all internal data structures used during the compilation, especially the node cache. Algorithms on BDDs always require the kernel which was used to compile the BDD. All fields of the kernel are private since there should be no reason ever to manually access or change them.

func NewKernel 

func NewKernel(fac f.Factory, numVars, nodeSize, cacheSize int32) *Kernel

NewKernel constructs a newBdd BDD kernel with numVars the number of variables on the kernel, nodeSize the initial number of nodes in the internal node table, and cacheSize the fixed size of the internal node cache.

func NewKernelWithOrdering 

func NewKernelWithOrdering(fac f.Factory, ordering []f.Variable, nodeSize, cacheSize int32) *Kernel

NewKernelWithOrdering constructs a newBdd BDD kernel with ordering the list of ordered variables, nodeSize the initial number of nodes in the internal node table, and cacheSize the fixed size of the internal node cache.

func (*Kernel) ActivateReorderDuringBuild 

func (k *Kernel) ActivateReorderDuringBuild(method ReorderingMethod, bound int32)

ActivateReorderDuringBuild activates automatic reordering during the BDD compilation process with the given reordering method and an upper bound for the number of reorderings performed.

func (*Kernel) AddAllVariablesAsBlock 

func (k *Kernel) AddAllVariablesAsBlock()

AddAllVariablesAsBlock adds a single variable block for all variables known by the kernel.

func (*Kernel) AddVariableBlock 

func (k *Kernel) AddVariableBlock(first, last int32, fixed bool)

AddVariableBlock adds a variable block starting at variable first and ending in variable last (both inclusive).

Variable blocks are used in the BDD reordering or in the automatic reordering during the construction of the BDD (configured by ActivateReorderDuringBuild). Variable blocks can be nested, i.e. one block can contain an arbitrary number of ("child") blocks. Furthermore, a variable block can also be a single variable.

During reordering, the child blocks of a parent block can be reordered, but they are kept together. So no other block can be moved in between the child blocks. Furthermore, variables in a block which are not in a child block will be left untouched.

Example: Lets assume we have a BDD with the variable ordering v1, v2, v3, v4, v5, v6, v7 We create the following blocks: 

A  reaching from v1 to v5
B  reaching from v6 to v7
A1 reaching from v1 to v2
A2 reaching from v3 to v3
A3 reaching from v4 to v5

This means that the variables of A and B can never be mixed up in the order. So during reordering the variables v6 and v7 can either be moved to the front (before A) or remain at their position. Furthermore, for example v1 and v2 will always stay together and neither v3 nor any other variable can be moved in between them. On the other hand, the blocks A1, A2, and A3 can be swapped arbitrarily.

These are valid result of a reordering based on the above blocks: 

v3, v1, v2, v4, v5, v6, v7
v6, v7, v4, v5, v3, v1, v2
v6, v7, v1, v2, v3, v4, v5

These however would be illegal: 

v2, v1, v3, v4, v5, v6, v7 (variables in a block which are not in a child block will not be reordered)
v1, v3, v2, v4, v5, v6, v7 (variables of different block will not be mixed up)

If a block is fixed (the example above assumed always blocks which are not fixed), its immediate child blocks will remain in their order. E.g. if block A was fixed, the blocks A1, A2, and A3 would not be allowed to be swapped. Let's assume block A to be fixed and that we have two other unfixed blocks: 

A11 reaching from v1 to v1
A12 reaching from v2 to v2

These are examples for legal reorderings: 

v2, v1, v3, v4, v5, v6, v7 (block A is fixed, but "grandchildren" are still allowed to be reordered)
v6, v7, v2, v1, v3, v4, v5

These are examples for illegal reorderings: 

v3, v2, v1, v4, v5, v6, v7 (block A is fixed, so it's child blocks must be reordered)
v1, v2, v4, v5, v3, v6, v7

Each block (including all nested blocks) must be defined by a separate call to this method. The blocks may be added in an arbitrary order, so it is not required to add them top-down or bottom-up. However, the blocks must not intersect, except of one block containing the other. Furthermore, both the first and the last variable must be known by the kernel and the level first must be lower than the level of last.

func (*Kernel) Factory 

func (k *Kernel) Factory() f.Factory

Factory() returns the formula factory of the kernel.

func (*Kernel) IndexForVariable 

func (k *Kernel) IndexForVariable(variable f.Variable) (int32, error)

IndexForVariable returns the kernel's internal index for the given variable. Returns an error if the given variable is not found on the kernel.

func (*Kernel) Reorder 

func (k *Kernel) Reorder(method ReorderingMethod)

Reorder reorders the variables on the kernel with the given reordering method. Beware that if the kernel was used for multiple BDDs, the reordering is performed on all of these BDDs.

Only blocks of variables will be reordered. See the documentation of AddVariableBlock to learn more about such variable blocks. Without the definition of any block, nothing will be reordered.

If the reordering should be performed without any restrictions, AddVariableBlockAll can be called before this method.

func (*Kernel) Statistics 

func (k *Kernel) Statistics() Statistics

Statistics returns the statistics for the kernel.

func (*Kernel) SwapVariables 

func (k *Kernel) SwapVariables(first, second f.Variable) error

SwapVariables swaps the two variables first and second on the kernel. Beware that if the kernel was used for multiple BDDs, the variables are swapped in all of these BDDs. Returns an error if one of the variables cannot be found on the kernel.

type Node added in v0.4.0 

type Node interface {
	// Label returns the label of the node.  Can either be a variable or a constant.
	Label() string

	// Reports whether the node is an inner node.
	InnerNode() bool

	// Low returns the node of the low edge or nil for a terminal node.
	Low() Node

	// High returns the node of the high edge or nil for a terminal node.
	High() Node

	String() string
}

Node represents a node in a BDD.

type NodesHandler 

type NodesHandler struct {
	handler.Computation
	// contains filtered or unexported fields
}

A NodesHandler aborts the BDD compilation dependent on the number of nodes which are generated during the compilation.

func HandlerWithNodes 

func HandlerWithNodes(bound int) *NodesHandler

HandlerWithNodes returns a new BDD NodesHandler for the given bound of BDD nodes.

func (*NodesHandler) NewRefAdded 

func (n *NodesHandler) NewRefAdded() bool

NewRefAdded is called by the BDD compiler everytime a new BDD node reference is added.

type ReorderingMethod 

type ReorderingMethod byte
const (
	ReorderNone    ReorderingMethod = iota // no reordering
	ReorderWin2                            // sliding window of size 2
	ReorderWin2Ite                         // sliding window of size 2 iterative
	ReorderSift                            // sifting
	ReorderSiftIte                         // iterative sifting
	ReorderWin3                            // sliding window of size 3
	ReorderWin3Ite                         // sliding window of size 3 iterative
	ReorderRandom                          // random reordering (should only be used for testing)
)

func (ReorderingMethod) String 

func (i ReorderingMethod) String() string

type Statistics 

type Statistics struct {
	Produced int   // number of produced nodes
	Nodes    int32 // number of allocated nodes in the node table
	Free     int32 // number of free nodes in the node table
	Vars     int32 // number of variables
	Cache    int32 // cache size
	GC       int32 // number of performed garbage collections
	Used     int32 // number of used nodes
}

Statistics holds fields with internal kernel statistics.

type TimeoutHandler 

type TimeoutHandler struct {
	handler.Timeout
}

A TimeoutHandler aborts the BDD compilation dependent on the time it takes to generate the BDD.

func HandlerWithTimeout 

func HandlerWithTimeout(timeout handler.Timeout) *TimeoutHandler

HandlerWithTimeout returns a new BDD TimoutHandler for the given timout.

func (*TimeoutHandler) NewRefAdded 

func (t *TimeoutHandler) NewRefAdded() bool

NewRefAdded is called by the BDD compiler everytime a new BDD node reference is added.

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.