LogicCircuits.jl

This package provides basic functionality for doing logical reasoning using logical circuits. It has the stand-alone functionality illustrated below, and it serves as the logical foundations for other Juice packages (Julia Circuit Empanada).

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."

Advanced functionality

LogicCircuits further provides

• CPU (SIMD) and GPU (CUDA) kernels to efficiently compute satisfiability, model counts, etc., for large numbers of inputs, parallelizing over both circuit nodes and data inputs.
• Algorithms that transform circuits in non-trivial ways (split, clone, smooth, condition, etc.), verify and enforce structural properties.
• Functionality to load and save circuits in various file formats

Please see or for further details.

Development

If you are interested in modifying the package please see the development readme.

Acknowledgements

To acknowledge this package, please cite:

@inproceedings{DangAAAI21,
    title   = {Juice: A Julia Package for Logic and Probabilistic Circuits},
    author = {Dang, Meihua and Khosravi, Pasha and Liang, Yitao and Vergari, Antonio and Van den Broeck, Guy},
    booktitle = {Proceedings of the 35th AAAI Conference on Artificial Intelligence (Demo Track)},
    year    = {2021}
}