Edit on GitHub

LogicCircuits

LogicCircuits.Bdd — Type

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.BitCircuit — Type

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.GateType — Type

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
LogicCircuits.PlainStructConstantNode — Type

A plain structured logical constant leaf node, representing true or false. These are the only structured nodes that don't have an associated vtree node (cf. SDD file format)

source
LogicCircuits.SddConstantNode — Type

A SDD logical constant leaf node, representing true or false. These are the only structured nodes that don't have an associated vtree node (cf. SDD file format)

source
Base.:!= — Method

Returns whether the two given boolean functions are not equivalent.

source
Base.:== — Method

Returns whether the two given boolean functions are equivalent.

source
Base.:| — Method

Returns a new reduced Bdd restricted to instantiation X.

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

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

source
Base.hash — Method
hash(α::Bdd, h::UInt)::UInt

Returns a unique hash for the whole BDD.

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

Merge two circuits.

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

Read CNF/DNF from file.

source
Base.read — Method
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.sign — Method

Returns 0 if x is not a literal; else returns the literal's sign.

source
Base.split — Method
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.write — Method
Base.write(file::AbstractString, circuit::LogicCircuit)

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

source
Base.write — Method
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.write — Method
Base.write(io::IO, fnf::LogicCircuit, ::FnfFormat)

Write CNF/DNF to file.

source
Base.write — Method
Base.write(files::Tuple{AbstractString,AbstractString}, circuit::StructLogicCircuit)

Saves circuit and vtree to file.

source
DirectedAcyclicGraphs.foldup — Method
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_aggregate — Method
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.lca — Method

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
(¬)(x::Integer)::Bdd
(¬)(x::Bool)::Bool

Negates this boolean function.

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.and — Method
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.apply_step — Method

Recursively computes α ⊕ β. If the result was already computed as an intermediate result, return the cached result in T.

source
LogicCircuits.atmost — Method

Constructs a BDD mapping to true if at most n literals in L are in the input; otherwise false.

source
LogicCircuits.conjoin — Method
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.culledfreqs — Method

Returns an approximation (does not account for some repeated nodes) of how many times each variable is mentioned in α.

source
LogicCircuits.forget — Method
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.forget — Method
forget(root::LogicCircuit, is_forgotten::Function)

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

source
LogicCircuits.from_npbc — Method

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_literals — Function
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.infer_vtree — Function
infer_vtree(root::LogicCircuit)::Vtree

Infer circuits vtree if the circuit is struct-decomposable. Otherwise return nothing.

source
LogicCircuits.is_atom — Method
is_atom(α::Bdd)::Bool

Returns whether the given Bdd node is an atomic formula (i.e. a variable, ⊥, ⊤, or literal).

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

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

source
LogicCircuits.isdeterministic — Function
isdeterministic(root::LogicCircuit)::Bool

Is the circuit determinstic? Note: this function is generally intractable for large circuits.

source
LogicCircuits.issatisfiable — Method
issatisfiable(root::LogicCircuit)::Bool

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

source
LogicCircuits.istautology — Method

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.lit_val — Method

Returns whether a variable x appears as a positive literal in α, given that α is a conjunction of literals.

source
LogicCircuits.load — Method

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_count — Function
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.normal_form — Method

Runs a BFS on the mapping of parents, starting from either a ⊤ (true) or ⊥ (false) in order to find the corresponding CNF or DNF encoding.

source
LogicCircuits.or — Method
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_nf — Method

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 — Method

Check equivalence using probabilistic equivalence checking. Note that this implentation may not have any formal guarantees as such.

source
LogicCircuits.prob_equiv_signature — Function
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_mnist — Function

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.reduce! — Method

Reduce a Bdd rooted at α inplace, removing duplicate nodes and redundant sub-trees. Returns canonical representation of α.

source
LogicCircuits.respects_vtree — Method

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_prob — Function
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_bdd — Method

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.shannon! — Method

Performs Shannon's Decomposition on the Bdd α, given a set of variables to isolate. Any decomposition that results in a ⊥ is discarded.

source
LogicCircuits.smooth — Method
smooth(root::StructLogicCircuit)::StructLogicCircuit

Create an equivalent smooth circuit from the given circuit.

source
LogicCircuits.smooth_node — Method
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_node — Method
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_candidates — Method
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_circuit — Method

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_datasets — Method
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
LogicCircuits.zoo_cnf — Method
zoo_cnf(name)

Loads CNF file with given name from model zoo. See https://github.com/UCLA-StarAI/Circuit-Model-Zoo.

source
LogicCircuits.zoo_dnf — Method
zoo_dnf(name)

Loads DNF file with given name from model zoo. See https://github.com/UCLA-StarAI/Circuit-Model-Zoo.

source
LogicCircuits.zoo_jlc — Method
zoo_jlc(name)

Loads JLC file with given name from model zoo. See https://github.com/UCLA-StarAI/Circuit-Model-Zoo.

source
LogicCircuits.zoo_nnf — Method
zoo_nnf(name)

Loads NNF file with given name from model zoo. See https://github.com/UCLA-StarAI/Circuit-Model-Zoo.

source
LogicCircuits.zoo_sdd — Method
zoo_sdd(name)

Loads SDD file with given name from model zoo. See https://github.com/UCLA-StarAI/Circuit-Model-Zoo.

source
LogicCircuits.zoo_vtree — Method
zoo_vtree(name)

Loads Vtree file with given name from model zoo. See https://github.com/UCLA-StarAI/Circuit-Model-Zoo.

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

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

source
TikzGraphs.plot — Method
TikzGraphs.plot(vtree::Vtree)

Plots a vtree using TikzGraphs. Need to have LaTeX installed.

source