# 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}
}
```