Tranformations

In this section, we go over definition of possible transformations and code snippets to use them LogicCircuits.jl. We will use the following circuit(s) in our examples.

using LogicCircuits
X1, X2, X3 = pos_literals(LogicCircuit, 3)
circuit = (X1 & (X2 | -X3)) | (-X1 & (-X2 | X3));

tree_formula_string(circuit)

"((1 ⋀ (2 ⋁ -3)) ⋁ (-1 ⋀ (-2 ⋁ 3)))"

Forgetting

Given the logical formula of the circuit $\Delta$, forgetting the variable $X$ can be thought of as erasing (forgetting) what the formula says about variable $X$:

Forgeting is also equivalent to disjunction of different ways to condition on $X$. The possible values for $X$ are the literals $x$ or $\lnot x$, so we have:

Given a circuit you can use forget to forget a variable (or multiple variables). For example, let's forget $X_1$:

f1 = forget(circuit, (i) -> (i == Var(1)));

tree_formula_string(f1)

"((true ⋀ (2 ⋁ -3)) ⋁ (true ⋀ (-2 ⋁ 3)))"

Propagate Constants

Some circuits might have constants True or False in them. To remove the constants and simplifying the circuits we can use propagate_constants.

f1_prop = propagate_constants(f1);

tree_formula_string(f1_prop)

"(((2 ⋁ -3)) ⋁ ((-2 ⋁ 3)))"

Smoothing

Smoothing is the act of converting a non-smooth circuit to a circuit representing the same formula that is smooth. A logic circuit is smooth if each of its OR nodes are smooth. An OR node is smooth if all of its children mention the same variables.

Given a non-smooth circuit we can smooth it, for example:

nonsmooth_circuit = X1 | -X2
tree_formula_string(nonsmooth_circuit)

"(1 ⋁ -2)"

smooth_circuit = smooth(nonsmooth_circuit)
tree_formula_string(smooth_circuit)

"((1 ⋀ (2 ⋁ -2)) ⋁ (-2 ⋀ (1 ⋁ -1)))"

Split

Given the logical formula of the circuit $\Delta$ and a variable $x$, splitting would give us the following logical circuit:

c1 = |((X1 | -X1) & (X2 | -X2));
c2, _ = split(c1, (c1, c1.children[1]), Var(1); depth = 2);
plot(c1)

plot(c2)

Clone

Clone an or node and redirect one of its parents to the new copy. See clone for more documentation.

or = X1 | -X1
and1, and2 = (&)(or), (&)(or)
c1 = and1 | and2
c2 = clone(c1, and1, and2, or)
plot(c1)

plot(c2)

Merge

Merges two circuits. See merge for more documentation.

or1 = X1 | (-X1 & -X2)
or2 = -X1 | -X2
c1 = |(or1 & or2)
c2 = merge(c1, or1, or2)
plot(c1)

plot(c2)

Standardize Circuit

Standraizes a given circuit to make sure the following properties hold:

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

See standardize_circuit for more details.

Apply

Given two logic circuits $\Delta_1$, $\Delta_2$, and a binary operation $o$ the apply operation outputs a logic circuit representing:

Note that, in addition to representing the correct formula, the apply operation also wants to preserve the structural properites of the circuits such as determinism and decomposability.

The major binary operations are conjunction ($\land$), disjunction ($\lor$), and XOR ($\oplus$). There are $2^4 = 16$ possible binary operations, $6$ of which are trivial operations (such as always returning $false$ or depending only on one of the circuits). The other $10$ can be derived by combination of not operation ($\lnot$) with the main 3 operations mentioned. The list of all possible non-trivial binary operations are below:

Misc

The following are also useful circuit transformation:

• deepcopy: Recursively create a copy circuit rooted at n to a certain depth depth.
• replace_node: Replaces node old with node new in the circuit.
• split_candidates: Return a list of possible split candidates
• clone_candidates: Returns a list of possible clone candidates
• random_split: Randomly picking egde and variable from split candidates