# LogicCircuits

LogicCircuits.BddType

A Binary Decision Diagram.

• index: the vertex variable (-1 if terminal vertex
• low: low child vertex of BDD (undef if terminal vertex)
• high: high child vertex of BDD (undef if terminal vertex)
• value: terminal boolean value
• id: unique identifier
source
LogicCircuits.BitCircuitType

A bit circuit is a low-level representation of a logical circuit structure.

They are a "flat" representation of a circuit, essentially a bit string, that can be processed by lower level code (e.g., GPU kernels)

The wiring of the circuit is captured by two matrices: nodes and elements.

• Nodes are either leafs or decision (disjunction) nodes in the circuit.
• Elements are conjunction nodes in the circuit.
• In addition, there is a vector of layers, where each layer is a list of node ids. Layer 1 is the leaf/input layer. Layer end is the circuit root.
• And there is a vector of parents, pointing to element id parents of decision nodes.

Nodes are represented as a 4xN matrix where

• nodes[1,:] is the first element id belonging to this decision
• nodes[2,:] is the last element id belonging to this decision
• nodes[3,:] is the first parent index belonging to this decision
• nodes[4,:] is the last parent index belonging to this decision

Elements belonging to node i are elements[:, nodes[1,i]:nodes[2,i]] Parents belonging to node i are parents[nodes[3,i]:nodes[4,i]]

Elements are represented by a 3xE matrix, where

• elements[1,:] is the decision node id (parents of the element),
• elements[2,:] is the prime node id (child of the element)
• elements[3,:] is the sub node id (child of the element)
source
LogicCircuits.GateTypeType

A trait hierarchy denoting types of nodes GateType defines an orthogonal type hierarchy of node types, not circuit types, so we can dispatch on node type regardless of circuit type. See @ref{https://docs.julialang.org/en/v1/manual/methods/#Trait-based-dispatch-1}

source
Base.deepcopyFunction
deepcopy(n::LogicCircuit, depth::Int64)

Recursively create a copy circuit rooted at n to a certain depth depth

source
Base.mergeMethod
merge(root::LogicCircuit, or1::LogicCircuit, or2::LogicCircuit)

Merge two circuits.

source
Base.readMethod
Base.read(io::IO, ::Type{PlainLogicCircuit}, ::FnfFormat)

source
Base.readMethod
Base.read(file::AbstractString, ::Type{C}) where C <: LogicCircuit

Reads circuit from file; uses extension to detect format type, for example ".sdd" for SDDs.

source
Base.splitMethod
split(root::LogicCircuit, (or, and)::Tuple{LogicCircuit, LogicCircuit}, var::Var; depth=0, sanity_check=true)

Return the circuit after spliting on edge edge and variable var

source
Base.writeMethod
Base.write(file::AbstractString, circuit::LogicCircuit)

Writes circuit to file; uses file name extention to detect file format.

source
Base.writeMethod
write(file::AbstractString, vtree::PlainVtree)

Saves a vtree in the given file path based on file format. Supported formats:

• ".vtree" for Vtree files
• ".dot" for dot files
source
Base.writeMethod
Base.write(files::Tuple{AbstractString,AbstractString}, circuit::StructLogicCircuit)

Saves circuit and vtree to file.

source
DirectedAcyclicGraphs.foldupMethod
foldup(node::LogicCircuit,
f_con::Function,
f_lit::Function,
f_a::Function,
f_o::Function)::T where {T}

Compute a function bottom-up on the circuit. f_con is called on constant gates, f_lit is called on literal gates, f_a is called on conjunctions, and f_o is called on disjunctions. Values of type T are passed up the circuit and given to f_a and f_o through a callback from the children.

source
DirectedAcyclicGraphs.foldup_aggregateMethod
foldup_aggregate(node::LogicCircuit,
f_con::Function,
f_lit::Function,
f_a::Function,
f_o::Function,
::Type{T})::T where T

Compute a function bottom-up on the circuit. f_con is called on constant gates, f_lit is called on literal gates, f_a is called on conjunctions, and f_o is called on disjunctions. Values of type T are passed up the circuit and given to f_a and f_o in an aggregate vector from the children.

source
DirectedAcyclicGraphs.lcaMethod

Compute the lowest common ancestor of two vtree nodes Warning: this method uses an incomplete varsubset check for descends_from and is only correct when v and w are part of the same larger vtree.

source
LogicCircuits.:∧Method
(∧)(α::Bdd, β::Bdd)::Bdd
(∧)(x::Integer, β::Bdd)::Bdd
(∧)(α::Bdd, x::Integer)::Bdd
(∧)(x::Integer, y::Integer)::Bdd
(∧)(x::Bool, y::Bool)::Bool

Returns a conjunction over the given boolean functions.

source
LogicCircuits.:∨Method
(∨)(α::Bdd, β::Bdd)::Bdd
(∨)(x::Integer, β::Bdd)::Bdd
(∨)(α::Bdd, x::Integer)::Bdd
(∨)(x::Integer, y::Integer)::Bdd
(∨)(x::Bool, y::Bool)::Bool

Returns a disjunction over the given boolean functions.

source
LogicCircuits.andMethod
and(α::Bdd, β::Bdd)::Bdd
and(x::Integer, β::Bdd)::Bdd
and(α::Bdd, x::Integer)::Bdd
and(x::Integer, y::Integer)::Bdd
and(Φ::Vararg{Bdd})::Bdd
and(Φ::AbstractVector{Bdd})::Bdd
and(Φ::Vararg{T})::Bdd where T <: Integer
and(Φ::AbstractVector{T})::Bdd where T <: Integer
and(Φ::Vararg{Union{T, Bdd}})::Bdd where T <: Integer

Returns a conjunction over the given boolean functions.

source
LogicCircuits.conjoinMethod
conjoin(root::LogicCircuit, lit::Lit; callback::Function)

Return the circuit conjoined with th given literal constrains callback is called after modifying conjunction node

source
LogicCircuits.forgetMethod
forget(α::Bdd, x::Integer)::Bdd = eliminate(α, x)
forget(α::Bdd, X::Union{Set, BitSet, AbstractVector{T}}) where T <: Integer

Returns the resulting BDD after applying the forget operation. Equivalent to $\phi|_x \vee \phi|_{\neg x}$.

source
LogicCircuits.forgetMethod
forget(root::LogicCircuit, is_forgotten::Function)

Forget variables from the circuit. Warning: this may or may not destroy the determinism property.

source
LogicCircuits.from_npbcMethod

Translates a cardinality constraint in normal pseudo-boolean constraint form into a BDD.

Since cardinality constraints correspond to having coefficients set to one, we ignore the C's.

Argument L corresponds to the vector of literals to be chosen from; b is how many literals in L are selected.

See Eén and Sörensson 2006.

source
LogicCircuits.implied_literalsFunction
implied_literals(root::LogicCircuit)::Union{BitSet, Nothing}

Compute at each node literals that are implied by the formula. nothing at a node means all literals are implied (i.e. the node's formula is false)

This algorithm is sound but not complete - all literals returned are correct, but some true implied literals may be missing.

source
LogicCircuits.iscanonicalMethod
iscanonical(circuit::LogicCircuit, k::Int; verbose = false)

Does the given circuit have canonical Or gates, as determined by a probabilistic equivalence check?

source
LogicCircuits.issatisfiableMethod
issatisfiable(root::LogicCircuit)::Bool

Determine whether the logical circuit is satisfiable (has a satisfying assignment). Requires decomposability of the circuit.

source
LogicCircuits.istautologyMethod

istautology(root::LogicCircuit)::Bool

Determine whether the logical circuit is a tautology (every assignment satisfies it; the sentence is valid). Requires decomposability and determinism of the circuit.

source
LogicCircuits.loadMethod

Loads a BDD from given file.

Supported file formats:

• CNF (.cnf);
• DNF (.dnf);
• BDD (.bdd).

To load as any of these file formats, simply set the filename with the desired extension.

Keyword arguments are passed down to the open function.

source
LogicCircuits.model_countFunction
model_count(root::LogicCircuit, num_vars_in_scope::Int = num_variables(root))::BigInt

Get the model count of the circuit. The num_vars_in_scope is set to number of variables in the circuit, but sometimes need to set different values, for example, if not every variable is mentioned in the circuit.

source
LogicCircuits.orMethod
or(α::Bdd, β::Bdd)::Bdd
or(x::Integer, β::Bdd)::Bdd
or(α::Bdd, x::Integer)::Bdd
or(x::Integer, y::Integer)::Bdd
or(Φ::Vararg{Bdd})::Bdd
or(Φ::AbstractVector{Bdd})::Bdd
or(Φ::Vararg{T})::Bdd where T <: Integer
or(Φ::AbstractVector{T})::Bdd where T <: Integer
or(Φ::Vararg{Union{T, Bdd}})::Bdd where T <: Integer

Returns a disjunction over the given boolean functions.

source
LogicCircuits.print_nfMethod

Pretty print BDD as a normal form (CNF or DNF).

Caution: may exponentially explode.

Alternatively, pretty prints using the given glyphs (default ∧, ∨ and ¬).

ϕ = (1 ∧ ¬2) ∨ (2 ∧ 3)
print_nf(α; out = false)
ϕ = (1 ∧ ¬2) ∨ (2 ∧ 3)
print_nf(α; out = false, which = "dnf", glyphs = ['+', '*', '-'])
source
LogicCircuits.prob_equiv_signatureFunction
prob_equiv_signature(circuit::LogicCircuit, k::Int)

Get a signature for each node using probabilistic equivalence checking. Note that this implentation may not have any formal guarantees as such.

source
LogicCircuits.process_mnistFunction

Processes the mnist dataset using the MNIST object from MLDataSets package MLDS_MNIST = the MNIST from MLDataSets labeled = whether to return the lables

source
LogicCircuits.respects_vtreeMethod

Does the circuit respect the given vtree? This function allows for constants in conjunctions, but only when a vtree node can be found where the left and right conjunct can be assigned to the left and right vtree.

source
LogicCircuits.sat_probFunction
sat_prob(root::LogicCircuit; varprob::Function)::Rational{BigInt}

Get the probability that a random world satisties the circuit. Probability of each variable is given by varprob Function which defauls to 1/2 for every variable.

source
LogicCircuits.save_bddMethod

Saves a BDD as a file.

Supported file formats:

• CNF (.cnf);
• DNF (.dnf);
• BDD (.bdd).

To save as any of these file formats, simply set the filename with the desired extension.

Keyword arguments are passed down to the open function.

source
LogicCircuits.smooth_nodeMethod
smooth_node(node::LogicCircuit, missing_scope, lit_nodes)

Return a smooth version of the node where the missing_scope variables are added to the scope, using literals from lit_nodes

source
LogicCircuits.smooth_nodeMethod
smooth_node(node::StructLogicCircuit, parent_scope, scope, lit_nodes, vtree_leaves)

Return a smooth version of the node where the are added to the scope by filling the gap in vtrees, using literals from lit_nodes

source
LogicCircuits.split_candidatesMethod
split_candidates(circuit::LogicCircuit)::Tuple{Vector{Tuple{LogicCircuit, LogicCircuit}}, Dict{LogicCircuit, BitSet}}

Return the edges and variables which can be splited on

source
LogicCircuits.standardize_circuitMethod

Standardize the circuit:

1. Children of or nodes are and nodes.
2. Children of and nodes are or nodes.
3. Each and node has exactly two children.

Note: for circuits with parameters this function will not keep the parameters equavalent.

source
LogicCircuits.twenty_datasetsMethod
train, valid, test = twenty_datasets(name)

Load a given dataset from the density estimation datasets. Automatically downloads the files as julia Artifacts. See https://github.com/UCLA-StarAI/Density-Estimation-Datasets for a list of avaialble datasets.

source
TikzGraphs.plotMethod
TikzGraphs.plot(lc::LogicCircuit; simplify=false)

Plots a LogicCircuit using TikzGraphs. Needt o have LaTeX installed.

source