Edit on GitHub

Queries

Evaluation

Given a logic circuit $\Delta$ and an assignment to its variable, we would like to know the output of the circuit. For example, if $\Delta = X \land Y$, and we assign $x$, $\lnot y$:

\[X \land Y = \text{true} \land \text{false} = \text{false}\]
lc = zoo_sdd("random.sdd");
X = rand(Bool, num_variables(lc));

lc(X)
false

Satisfiability

Given a logic circuit $\Delta$, the goal of SAT is to answer whether there is an assignment to its variables such that the output is true. Depending on the structural properties of the logic circuit this problem can be intractable or tractable.

We can use sat_prob to compute probability of a random world satisfying the circuit. Note that sat_prob assumes that we have a smooth, deterministic, and decomposable circuit.

lc = zoo_sdd("random.sdd");
prob = sat_prob(lc);
Float64(prob)
6.103515625e-5

By default, every postive literal $x_i$ has probability 1/2, we can set probability of literal values to any constant probabilities, for example:

prob = sat_prob(lc; varprob = (i) -> BigInt(1) // BigInt(3));
Float64(prob)
0.001783492321326371

Model Counting

Given a logic circuit $\Delta$, the goal of model counting is to count how many ways there are to assign values to variables of $\Delta$ such that the output of the circuit is true. Note that model_count assumes we have a smooth, deterministic, and decomposable circuit.

lc = smooth(zoo_sdd("random.sdd"));
model_count(lc)
65536

Let's see how conjoining affects the model count. Observe that model count of $\Delta$ should equal to adding model counts of $\Delta \mid x_2$ and $\Delta \mid \lnot x_2$.

c2 = conjoin(lc, Lit(2));
c2not = conjoin(lc, Lit(-2));
model_count(c2, num_variables(lc)), model_count(c2not, num_variables(lc))
(32768, 32768)

Note that some transformations lead to losing required properties needed for tractable model count. For example, after forgetting variables we lose determinism and hence cannot use model_count anymore.

Equivalence Checking

Given two logic circuits $\Delta_1$ and $\Delta_2$, the goal is to check whether these two circuits represent the same formula. There are both determnistic and probabilistic algorithms for this task.

Misc

Here are few other useful queries. Look inside thier documentation for more details.