IncidenceGraph - Maple Help

Home : Support : Online Help : Mathematics : Logic : IncidenceGraph

Logic

 IncidenceGraph
 construct incidence graph for Boolean expression
 PrimalGraph
 construct primal graph for Boolean expression

 Calling Sequence IncidenceGraph(expr, opts) PrimalGraph(expr, opts)

Parameters

 expr - Boolean expression in conjunctive normal form opts - (optional) zero or more options as specified below

Options

 • output=list or one of expressions or graph
 a list of one or more of the symbols expressions or group, or one of the symbols expressions or graph.
 The symbol graph corresponds to the graph of the requested type constructed from expr. (lead=indent) The symbol expressions is the list of variables and clauses of expr in the order specified in the output graph.
 • weighted=true or false
 If weighted=true, PrimalGraph returns a weighted graph where the weight of each edge between variables u and v is the number of clauses in which both u and v appear, divided by n*(n-1)/2 where n is the number of variables in expr. The default is false.
 Note this option is only supported for PrimalGraph.
 • datatype= one of float[4], float[8], or anything
 Specifies the data type of the weight matrix when weighted=true. When datatype=anything, the weight matrix contains exact rational numbers corresponding to the computed weighted. Otherwise, the entries will be floating-point numbers of the specified precision. The default is anything.
 Note this option is only supported for PrimalGraph and only has an effect if weighted'=true.

Description

 • The IncidenceGraph command computes the incidence graph of a given Boolean expression expr.
 • The PrimalGraph command computes the primal graph of a given Boolean expression expr.
 • The result of both commands is a Graph object and can be examined and visualized using the tools in the GraphTheory package.
 • The expression expr must be in conjunctive normal form (CNF). If not already in CNF, expr can be converted to CNF using Normalize; alternatively, Tseitin may be used to find an equisatifiable expression in CNF.

Definitions

 • A primal graph of a Boolean expression expr, also called the variable incidence graph is a graph whose vertices are the variables of expr. An edge exists between two variables if they occur together in a clause of expr, in either negated or non-negated form.
 • An incidence graph of a Boolean expression expr, also called the variable-clause incidence graph, is a bipartite graph whose vertex set is the union of the set of variables and the set of clauses of expr. An edge exists between a variable v and a clause c when c contains v or the negation of v as a literal.

Examples

Find the primal graph and incidence graph for a simple Boolean expression.

 > $\mathrm{with}\left(\mathrm{Logic}\right):$
 > $\mathrm{expr}≔\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}c\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(c\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}d\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}e\right)$
 ${\mathrm{expr}}{≔}\left({a}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{b}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{c}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({c}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{d}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{e}\right)$ (1)
 > $\mathrm{PG}≔\mathrm{PrimalGraph}\left(\mathrm{expr}\right)$
 ${\mathrm{PG}}{≔}{\mathrm{Graph 1: an undirected unweighted graph with 5 vertices and 6 edge\left(s\right)}}$ (2)
 > $\mathrm{GraphTheory}:-\mathrm{DrawGraph}\left(\mathrm{PG}\right)$
 > $\mathrm{IG}≔\mathrm{IncidenceGraph}\left(\mathrm{expr}\right)$
 ${\mathrm{IG}}{≔}{\mathrm{Graph 2: an undirected unweighted graph with 7 vertices and 6 edge\left(s\right)}}$ (3)
 > $\mathrm{GraphTheory}:-\mathrm{DrawGraph}\left(\mathrm{IG},\mathrm{style}=\mathrm{bipartite}\right)$

By invoking IncidenceGraph with the output option we can obtain the list L of subexpressions.

 > $\mathrm{expr}≔\left(x\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}y\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}z\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}x\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}y\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}z\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}x\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}y\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}z\right)$
 ${\mathrm{expr}}{≔}\left({x}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{y}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{z}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({x}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{y}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{z}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({x}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{y}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{z}\right)$ (4)
 > $G,L≔\mathrm{IncidenceGraph}\left(\mathrm{expr},\mathrm{output}=\left[\mathrm{graph},\mathrm{expressions}\right]\right)$
 ${G}{,}{L}{≔}{\mathrm{Graph 3: an undirected unweighted graph with 6 vertices and 9 edge\left(s\right)}}{,}\left[{x}{,}{y}{,}{z}{,}{x}{\vee }{y}{\vee }{z}{,}\left({¬}{x}\right){\vee }\left({¬}{y}\right){\vee }\left({¬}{z}\right){,}\left({¬}{x}\right){\vee }\left({¬}{y}\right){\vee }\left({¬}{z}\right)\right]$ (5)
 > $L$
 $\left[{x}{,}{y}{,}{z}{,}{x}{\vee }{y}{\vee }{z}{,}\left({¬}{x}\right){\vee }\left({¬}{y}\right){\vee }\left({¬}{z}\right){,}\left({¬}{x}\right){\vee }\left({¬}{y}\right){\vee }\left({¬}{z}\right)\right]$ (6)
 > $\mathrm{GraphTheory}:-\mathrm{DrawGraph}\left(G,\mathrm{style}=\mathrm{bipartite}\right)$

References

 Szeider S. (2008) "Parameterized SAT." In: Kao MY. (eds) Encyclopedia of Algorithms. Springer, Boston, MA. doi:10.1007/978-1-4939-2864-4_283

Compatibility

 • The Logic[IncidenceGraph] and Logic[PrimalGraph] commands were introduced in Maple 2020.