### Quick Tutorial

Assuming that the LogicCircuits Julia package has been installed with julia -e 'using Pkg; Pkg.add("LogicCircuits")', we can start using it as follows.

using LogicCircuits

### Reasoning with manually constructed circuits

We begin by creating three positive literals (logical variables) and manually constructing a simple circuit using logical connectives & (and), | (or), and - (not).

sun, rain, rainbow = pos_literals(LogicCircuit, 3)
circuit = (rainbow & sun & rain) | (-rainbow); # rainbow implies sun and rain

Just like any logical circuit or Boolean function, we can evaluate ours on various inputs.

circuit(false, true, true) # sun is false, rain is true, rainbow is true
false
circuit(true, true, true) # sun is true, rain is true, rainbow is true
true

The purpose of this package, however, is to enable more interesting inference scenarios. This is possible by ensuring that the circuit has certain properties, such as decomposability, determinism, and more. Our current circuit happens to already be decomposable and deterministic by construction:

isdecomposable(circuit) && isdeterministic(circuit)
true

The decomposability property ensures that we can ask whether the circuit is satisfiable (the classical SAT problem) and, surprisingly, still get our answer efficiently. Of course, from the input true, true, true tried above, we know the answer to be true.

issatisfiable(circuit) # does there exist an input that outputs true?
true

In addition, the determinism property allows us to efficiently decide whether the circuit is a tautology (always true), or compute its model count, that is, the number of satisfying assignments.

istautology(circuit) # do all inputs give the circuit output true?
false
model_count(circuit) # how many possible inputs give the output true?
5

### Reasoning with compiled circuits

As logical sentences become more complicated, it becomes infeasible to manually write down circuits that have the requisite properties that guarantee tractable inference.

A process called compilation can solve this problem. Concretely, LogicCircuits supports compilation into a particular type of circuit called SDD. We construct an SDD manager with four additional variables, and then ask to compile our running example circuit into an SDD:

manager = SddMgr(7, :balanced)
circuit = compile(manager, circuit);

Now we are able to incorporate many more logical sentences into the same circuit.

sun, rain, rainbow, cloud, snow, los_angeles, belgium = pos_literals(Sdd, manager, 7)
circuit &= (-los_angeles | -belgium) # cannot be in LA and Belgium at the same time
circuit &= (los_angeles ⇒ sun) ∧ (belgium ⇒ cloud) # unicode logical syntax
circuit &= (¬(rain ∨ snow) ⇐ ¬cloud); # no rain or snow without clouds

Incorporating these constraints has increased the size of our circuit.

plot(circuit; simplify=true)

Crucially, the circuit is still decomposable and deterministic.

isdecomposable(circuit) && isdeterministic(circuit)
true

This means that we can still decide satisfiability, count models, and solve various inference tasks efficiently. For example, we can compute the fraction of inputs that gives the output true:

sat_prob(circuit)
29//128

Moreover, compiled SDD circuits allow for efficiently checking whether one circuit logically entails another circuit, and whether two circuits are logically equivalent.

entails(circuit, (rainbow ⇒ cloud))
true
entails(circuit, (rainbow ⇒ belgium))
false
equivalent((rainbow ⇒ belgium), (¬belgium ⇒ ¬rainbow))
true

Logical constraints are often written in conjunctive normal form (CNF). These can be loaded from file and compiled into circuits, using an SDD manager whose decomposition structure is specified by a vtree file.

manager = SddMgr(zoo_vtree("iscas89/s208.1.scan.min.vtree"))
circuit = compile(manager, zoo_cnf("iscas89/s208.1.scan.cnf")) # CNF has 285 clauses
"This CNF has $(model_count(circuit)) satisfying assignments. Its circuit has$(num_nodes(circuit)) nodes and \$(num_edges(circuit)) edges."
"This CNF has 262144 satisfying assignments. Its circuit has 3115 nodes and 5826 edges."

LogicCircuits further provides