Online Help

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.

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.

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.

$\mathrm{with}\left(\mathrm{Logic}\right)\:$

$\mathrm{expr}≔\left(a\mathbf{or}b\mathbf{or}\mathbf{not}c\right)\mathbf{and}\left(c\mathbf{or}d\mathbf{or}\mathbf{not}e\right)$

$\mathrm{expr}≔\left(a\mathbf{or}b\mathbf{or}\mathbf{not}c\right)\mathbf{and}\left(c\mathbf{or}d\mathbf{or}\mathbf{not}e\right)$

$\mathrm{PG}≔\mathrm{PrimalGraph}\left(\mathrm{expr}\right)$

$\mathrm{PG}≔\mathrm{Graph\; 1:\; an\; undirected\; graph\; with\; 5\; vertices\; and\; 6\; edges}$

$\mathrm{GraphTheory}:-\mathrm{DrawGraph}\left(\mathrm{PG}\right)$

$\mathrm{IG}≔\mathrm{IncidenceGraph}\left(\mathrm{expr}\right)$

$\mathrm{IG}≔\mathrm{Graph\; 2:\; an\; undirected\; graph\; with\; 7\; vertices\; and\; 6\; edges}$

$\mathrm{GraphTheory}:-\mathrm{DrawGraph}\left(\mathrm{IG}\,\mathrm{style}=\mathrm{bipartite}\right)$

$\mathrm{expr}≔\left(x\mathbf{or}y\mathbf{or}z\right)\mathbf{and}\left(\mathbf{not}x\mathbf{or}\mathbf{not}y\mathbf{or}\mathbf{not}z\right)\mathbf{and}\left(\mathbf{not}x\mathbf{or}\mathbf{not}y\mathbf{or}\mathbf{not}z\right)$

$\mathrm{expr}≔\left(x\mathbf{or}y\mathbf{or}z\right)\mathbf{and}\mathbf{not}\left(x\mathbf{and}y\mathbf{and}z\right)\mathbf{and}\mathbf{not}\left(x\mathbf{and}y\mathbf{and}z\right)$

$G,L≔\mathrm{IncidenceGraph}\left(\mathrm{expr}\,\mathrm{output}=\left[\mathrm{graph}\,\mathrm{expressions}\right]\right)$

$G,L≔\mathrm{Graph\; 3:\; an\; undirected\; graph\; with\; 6\; vertices\; and\; 9\; edges},\left[x\,y\,z\,x\vee y\vee z\,\left(\neg x\right)\vee \left(\neg y\right)\vee \left(\neg z\right)\,\left(\neg x\right)\vee \left(\neg y\right)\vee \left(\neg z\right)\right]$

$L$

$\left[x\,y\,z\,x\vee y\vee z\,\left(\neg x\right)\vee \left(\neg y\right)\vee \left(\neg z\right)\,\left(\neg x\right)\vee \left(\neg y\right)\vee \left(\neg z\right)\right]$

$\mathrm{GraphTheory}:-\mathrm{DrawGraph}\left(G\,\mathrm{style}=\mathrm{bipartite}\right)$

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

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

For more information on Maple 2020 changes, see Updates in Maple 2020 .