Documentation
¶
Overview ¶
Package graph contains datastructures and algorithm for simple graph and hyper-graph implementations in LogicNG.
Hyper-graphs are only used for the BDD Force variable ordering heuristic. Graphs however are used in a more versatile manner for constraint graphs of formulas. With constraint graphs you often can split a problem in disjunctive sub-problems by computating their strongly connected components.
To generate a constraint graph from a set of formulas, you can call
constraintGraph := graph.GenerateConstraintGraph(fac, formulas)
You can then compute the strongly connected components and split the original formulas with respect to the constraint graph:
components := graph.ComputeConnectedComponents(constraintGraph) splittedFormulas := graph.SplitFormulasByComponent(fac, formulas, components)
Index ¶
- func ComputeConnectedComponents(graph *FormulaGraph) [][]f.Variable
- func GenerateGraphicalFormulaGraph(fac f.Factory, graph *FormulaGraph, generator *graphical.Generator[f.Formula]) *graphical.Representation
- func SplitFormulasByComponent(fac f.Factory, formulas []f.Formula, components [][]f.Variable) [][]f.Formula
- type FormulaGraph
- type Hypergraph
- type HypergraphEdge
- type HypergraphNode
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func ComputeConnectedComponents ¶
func ComputeConnectedComponents(graph *FormulaGraph) [][]f.Variable
ComputeConnectedComponents returns the strongly connected components of a constraint graph. Each component is represented as a slice of variables.
func GenerateGraphicalFormulaGraph ¶
func GenerateGraphicalFormulaGraph( fac f.Factory, graph *FormulaGraph, generator *graphical.Generator[f.Formula], ) *graphical.Representation
GenerateGraphicalFormulaGraph generates a graphical representation of the graph with the configuration of the generator. The resulting representation can then be exported as mermaid or graphviz graph.
func SplitFormulasByComponent ¶
func SplitFormulasByComponent(fac f.Factory, formulas []f.Formula, components [][]f.Variable) [][]f.Formula
SplitFormulasByComponent splits a given list of formulas with respect to a given list of components, usually from the constraint graph of the given formulas. The result contains one list of formulas for each of the given components. All formulas in this list have only variables from the respective component.
Types ¶
type FormulaGraph ¶
type FormulaGraph struct {
// contains filtered or unexported fields
}
A FormulaGraph represents a graph with nodes holding formulas.
func GenerateConstraintGraph ¶
func GenerateConstraintGraph(fac f.Factory, formulas ...f.Formula) *FormulaGraph
GenerateConstraintGraph generates a constraint graph for the given formulas. The nodes of the constraint graph hold all variables of the given formulas. Two variable nodes are connected if they occur in the same formula.
func NewFormulaGraph ¶
func NewFormulaGraph() *FormulaGraph
NewFormulaGraph generates a new empty formula graph.
func (*FormulaGraph) AddNode ¶
func (g *FormulaGraph) AddNode(formula f.Formula) int
AddNode adds a new formula to the graph if it is not already present and returns its internal index.
func (*FormulaGraph) Connect ¶
func (g *FormulaGraph) Connect(n1, n2 f.Formula)
Connect connects two formula nodes in the graph with an undirected edge.
func (*FormulaGraph) Neighbours ¶
func (g *FormulaGraph) Neighbours(node f.Formula) []f.Formula
Neighbours returns all formulas connected to the given node in the graph.
func (*FormulaGraph) Nodes ¶
func (g *FormulaGraph) Nodes() []f.Formula
Nodes returns all nodes - und thus formulas - of the graph.
type Hypergraph ¶
type Hypergraph struct {
Nodes []*HypergraphNode
Edges []*HypergraphEdge
}
A Hypergraph holds its nodes and edges.
func HypergraphFromCNF ¶
HypergraphFromCNF generates a hyper-graph from a CNF formula. Each variable is represented by a node in the hyper-graph, each clause is represented by a hyper-edge between all variables of the clause. Returns an error if the input is not in CNF.
func HypergraphFromClauses ¶
HypergraphFromClauses generates a hyper-graph from a CNF given as a list of clauses. Each variable is represented by a node in the hyper-graph, each clause is represented by a hyper-edge between all variables of the clause. Returns an error if the input is not in CNF.
func NewHypergraph ¶
func NewHypergraph() *Hypergraph
NewHypergraph generates a new empty hyper-graph.
func (*Hypergraph) AddEdge ¶
func (g *Hypergraph) AddEdge(nodes []*HypergraphNode)
AddEdge adds an edge between the given nodes.
type HypergraphEdge ¶
type HypergraphEdge struct {
Nodes []*HypergraphNode
}
A HypergraphEdge connects nodes in a hyper-graph.
func NewHypergraphEdge ¶
func NewHypergraphEdge(nodes []*HypergraphNode) *HypergraphEdge
NewHypergraphEdge returns a new edge connecting the given nodes.
type HypergraphNode ¶
type HypergraphNode struct {
Content f.Variable
Edges []*HypergraphEdge
}
A HypergraphNode represents a node holding a variable in a hyper-graph. It holds also a list of edges on which it occurs.
func NewHypergraphNode ¶
func NewHypergraphNode(graph *Hypergraph, variable f.Variable) *HypergraphNode
NewHypergraphNode returns a new node in the given graph with the given variable as content.
func (*HypergraphNode) ComputeTentativeNewLocation ¶
func (n *HypergraphNode) ComputeTentativeNewLocation(nodeOrdering *linkedhashmap.Map) float64
ComputeTentativeNewLocation is used in the Force orderings for BDDs.
Source Files