PySDD documentation

Python package for Sentential Decision Diagrams (SDD). Source available on https://github.com/wannesm/PySDD.

The SDD can be thought of as a “data structure” for representing Boolean functions, since SDDs are canonical and support a number of efficient operations for constructing and manipulating Boolean functions.

The open-source C SDD package allows users to construct, manipulate and optimize SDDs and is developed by Arthur Choi and Adnan Darwiche at UCLA’s Automated Reasoning Group. This Python wrapper is a collaboration between UCLA’s Automated Reasoning Group and KU Leuven’s Artificial Intelligence research group (DTAI).

Installation

Dependencies

  • Python >=3.6
  • Cython

Pip Installation

The package can be installed using Pip:

pip install pysdd

If the package complains that ModuleNotFoundError: No module named 'pysdd.sdd' something went wrong during compilation. Reinstall with the verbose option to see what the issue is:

pip install -vvv --upgrade --force-reinstall --no-deps --no-binary :all: pysdd

Compilation from Source

Notice: This wrapper requires some small changes to the SDD package. The changed files are already included in this repository. Do not overwrite them with the original files.

  • Download the SDD package from http://reasoning.cs.ucla.edu/sdd/.
  • Install the SDD package in the PySDD package in directories pysdd/lib/sdd-2.0 and pysdd/lib/sddlib-2.0 without overwriting the already available files.
  • Run python3 setup.py build_ext --inplace or make build to compile the library in the current directory. If you want to install the library such that the library is available for your local installation or in your virtual environment, use python3 setup.py install.

For some Linux platforms, it might be necessary to recompile the libsdd-2.0 code with the gcc option -fPIC and replace the pysdd/lib/sdd-2.0/lib/Linux/libsdd.a library with your newly compiled version.

Python package

The wrapper can be used as a Python package and allows for interactive use.

The following example builds an SDD for the formula a∧b ∨ b∧c ∨  c∧d.

from pysdd.sdd import SddManager, Vtree, WmcManager
vtree = Vtree(var_count=4, var_order=[2,1,4,3], vtree_type="balanced")
sdd = SddManager.from_vtree(vtree)
a, b, c, d = manager.vars

# Build SDD for formula
formula = (a & b) | (b & c) | (c & d)

# Model Counting
wmc = formula.wmc(log_mode=False)
print(f"Model Count: {wmc.propagate()}")
wmc.set_literal_weight(a, 0.5)
print(f"Weighted Model Count: {wmc.propagate()}")

# Visualize SDD and Vtree
with open("output/sdd.dot", "w") as out:
    print(formula.dot(), file=out)
with open("output/vtree.dot", "w") as out:
    print(vtree.dot(), file=out)

The SDD and Vtree are visualized using Graphviz DOT:

https://people.cs.kuleuven.be/wannes.meert/pysdd/sdd.png https://people.cs.kuleuven.be/wannes.meert/pysdd/vtree.png

More examples are available in the examples directory. An interactive Jupyter notebook is available in docs/examples.ipynb

Command Line Interface

A Python command line application is included with the package that can be used to perform SDD compilation and weighted model counting. This application mimicks the original sdd binary and adds additional features (e.g. weighted model counting).

The command line is accessible using one of three possible methods:

  • After installation using pip, the binary pysdd is available in your path.
  • If the package is available in PYTHONPATH, you can use python -m pysdd.
  • Run the pysdd-cli.py script that is available in the repository.

For example:

$ pysdd -h
$ python -m pysdd -h
$ ./pysdd-cli.py -h
usage: pysdd-cli.py [-h] [-c FILE | -d FILE | -s FILE] [-v FILE] [-W FILE]
                [-V FILE] [-R FILE] [-S FILE] [-m] [-t TYPE] [-r K] [-q]
                [-p] [--log_mode]

Sentential Decision Diagram, Compiler

optional arguments:
  -h, --help  show this help message and exit
  -c FILE     set input CNF file
  -d FILE     set input DNF file
  -s FILE     set input SDD file
  -v FILE     set input VTREE file
  -W FILE     set output VTREE file
  -V FILE     set output VTREE (dot) file
  -R FILE     set output SDD file
  -S FILE     set output SDD (dot) file
  -m          minimize the cardinality of compiled sdd
  -t TYPE     set initial vtree type (left/right/vertical/balanced/random)
  -r K        if K>0: invoke vtree search every K clauses. If K=0: disable
              vtree search. By default (no -r option), dynamic vtree search is
              enabled
  -q          perform post-compilation vtree search
  -p          verbose output
  --log_mode  weights in log

Weighted Model Counting is performed if the NNF file containts a line
formatted as follows: "c weights PW_1 NW_1 ... PW_n NW_n".

References

This package is inspired by the SDD wrapper used in the probabilistic programming language ProbLog.

References:

If you want to learn more about Sentential Decision Diagrams and Knowledge Compilation:

Bindings with other programming languages:

Contact

License

Copyright 2018, KU Leuven and Regents of the University of California.

The Python SDD wrapper is licensed under the Apache License, Version 2.0.

Build formula

Example 1: Build simple formula

#!/usr/bin/env python3
from pysdd.sdd import SddManager, Vtree


def main():
    # set up vtree and manager
    var_count = 4
    var_order = [2,1,4,3]
    vtree_type = "balanced"

    vtree = Vtree(var_count, var_order, vtree_type)
    manager = SddManager.from_vtree(vtree)

    # construct a formula (A^B)v(B^C)v(C^D)
    print("constructing SDD ... ")
    a, b, c, d = [manager.literal(i) for i in range(1, 5)]
    alpha = (a & b) | (b & c) | (c & d)
    print("done")

    print("saving sdd and vtree ... ")
    with open("output/sdd.dot", "w") as out:
        print(alpha.dot(), file=out)
    with open("output/vtree.dot", "w") as out:
        print(vtree.dot(), file=out)
    print("done")


if __name__ == "__main__":
    main()

Example 2: Garbage collection

#!/usr/bin/env python3
from pathlib import Path
from pysdd.sdd import SddManager, Vtree


def main():

  # set up vtree and manager
  var_count = 4
  vtree_type = "right".encode()
  vtree = Vtree(var_count=var_count, vtree_type=vtree_type)
  manager = SddManager(vtree=vtree)

  x = [None] + [manager.literal(i) for i in range(1,5)]

  # construct the term X_1 ^ X_2 ^ X_3 ^ X_4
  alpha =  x[1] &  x[2] & x[3] & x[4]

  # construct the term ~X_1 ^ X_2 ^ X_3 ^ X_4
  beta  = ~x[1] &  x[2] & x[3] & x[4]

  # construct the term ~X_1 ^ ~X_2 ^ X_3 ^ X_4
  gamma = ~x[1] & ~x[2] & x[3] & x[4]

  print("== before referencing:")
  print(f"  live sdd size = {manager.live_size()}")
  print(f"  dead sdd size = {manager.dead_size()}")

  # ref SDDs so that they are not garbage collected
  alpha.ref()
  beta.ref()
  gamma.ref()
  print("== after referencing:")
  print(f"  live sdd size = {manager.live_size()}")
  print(f"  dead sdd size = {manager.dead_size()}")

  # garbage collect
  manager.garbage_collect()
  print("== after garbage collection:");
  print(f"  live sdd size = {manager.live_size()}")
  print(f"  dead sdd size = {manager.dead_size()}")

  alpha.deref()
  beta.deref()
  gamma.deref()

  print("saving vtree & shared sdd ...")
  if not Path("output").is_dir():
      raise Exception(f"Directory 'output' does not exist")
  vtree.save_as_dot("output/shared-vtree.dot".encode())
  manager.shared_save_as_dot("output/shared.dot".encode())


if __name__ == "__main__":
    main()

Example 3: Minimization

#!/usr/bin/env python3
from pathlib import Path
from pysdd.sdd import SddManager, Vtree


def main():

  # set up vtree and manager
  vtree = Vtree.from_file("input/opt-swap.vtree".encode())
  manager = SddManager.from_vtree(vtree)

  print("reading sdd from file ...")
  alpha = manager.read_sdd_file("input/opt-swap.sdd".encode())
  print(f"  sdd size = {alpha.size()}")

  # ref, perform the minimization, and then de-ref
  alpha.ref()
  print("minimizing sdd size ... ", end="")
  manager.minimize()  # see also manager.minimize_limited()
  print("done!")
  print(f"  sdd size = {alpha.size()}")
  alpha.deref()

  # augment the SDD
  print("augmenting sdd ...")
  beta = alpha * (manager.l(4) + manager.l(5))
  print(f"  sdd size = {beta.size()}")

  # ref, perform the minimization again on new SDD, and then de-ref
  beta.ref()
  print("minimizing sdd ... ", end="")
  manager.minimize()
  print("done!")
  print(f"  sdd size = {beta.size()}")
  beta.deref()


if __name__ == "__main__":
    main()

Example 4: Vtree rotations

#!/usr/bin/env python3
from pathlib import Path
from pysdd.sdd import SddManager, Vtree


here = Path(__file__).parent


def main():

  # set up vtree and manager
  vtree = Vtree.from_file(bytes(here / "input" / "rotate-left.vtree"))
  manager = SddManager.from_vtree(vtree)

  # construct the term X_1 ^ X_2 ^ X_3 ^ X_4
  x = [None] + [manager.literal(i) for i in range(1, 5)]
  alpha = x[1]*x[2]*x[3]*x[4]

  # to perform a rotate, we need the manager's vtree
  manager_vtree = manager.vtree()
  manager_vtree_right = manager_vtree.right()

  print("saving vtree & sdd ...")
  if not Path("output").is_dir():
      raise Exception(f"Directory 'output' does not exist")
  manager_vtree.save_as_dot("output/before-rotate-vtree.dot".encode())
  alpha.save_as_dot("output/before-rotate-sdd.dot".encode())

  # ref alpha (so it is not gc'd)
  alpha.ref()

  # garbage collect (no dead nodes when performing vtree operations)
  print(f"dead sdd nodes = {manager.dead_count()}")
  print("garbage collection ...")
  manager.garbage_collect()
  print(f"dead sdd nodes = {manager.dead_count()}")

  print("left rotating ... ", end="")
  succeeded = manager_vtree_right.rotate_left(manager, 0)
  print("succeeded!" if succeeded == 1 else "did not succeed!")

  # deref alpha, since ref's are no longer needed
  alpha.deref()

  # the root changed after rotation, so get the manager's vtree again
  # this time using root_location
  manager_vtree = manager.vtree()

  print("saving vtree & sdd ...")
  if not Path("output").is_dir():
      raise Exception(f"Directory 'output' does not exist")
  manager_vtree.save_as_dot("output/after-rotate-vtree.dot".encode())
  alpha.save_as_dot("output/after-rotate-sdd.dot".encode())


if __name__ == "__main__":
    main()

Example 5: Modifying vtree

#!/usr/bin/env python3
from pathlib import Path
from pysdd.sdd import SddManager, Vtree


here = Path(__file__).parent


def main():

  # set up vtree and manager
  vtree = Vtree.from_file(bytes(here / "input" / "big-swap.vtree"))
  manager = SddManager.from_vtree(vtree)

  print("reading sdd from file ...")
  alpha = manager.read_sdd_file("input/big-swap.sdd".encode())
  print(f"  sdd size = {alpha.size()}")

  # to perform a swap, we need the manager's vtree
  manager_vtree = manager.vtree()

  # ref alpha (no dead nodes when swapping)
  alpha.ref()

  # using size of sdd normalized for manager_vtree as baseline for limit
  manager.init_vtree_size_limit(manager_vtree)

  limit = 2.0
  manager.set_vtree_operation_size_limit(limit)

  print(f"modifying vtree (swap node 7) (limit growth by {limit:.1f}x) ... ", end="")
  succeeded = manager_vtree.swap(manager, 1)  # limited
  print("succeeded!" if succeeded == 1 else "did not succeed!")
  print(f"  sdd size = {alpha.size()}")

  print("modifying vtree (swap node 7) (no limit) ... ", end="")
  succeeded = manager_vtree.swap(manager, 0)  # not limited
  print("succeeded!" if succeeded == 1 else "did not succeed!")
  print(f"  sdd size = {alpha.size()}")

  print("updating baseline of size limit ...")
  manager.update_vtree_size_limit()

  left_vtree = manager_vtree.left()
  limit = 1.2
  manager.set_vtree_operation_size_limit(limit)
  print(f"modifying vtree (swap node 5) (limit growth by {limit}x) ... ", end="")
  succeeded = left_vtree.swap(manager, 1)  # limited
  print("succeeded!" if succeeded == 1 else "did not succeed!")
  print(f"  sdd size = {alpha.size()}")

  limit = 1.3
  manager.set_vtree_operation_size_limit(limit)
  print(f"modifying vtree (swap node 5) (limit growth by {limit}x) ... ", end="")
  succeeded = left_vtree.swap(manager, 1)  # limited
  print("succeeded!" if succeeded == 1 else "did not succeed!")
  print(f"  sdd size = {alpha.size()}")

  # deref alpha, since ref's are no longer needed
  alpha.deref()

if __name__ == "__main__":
    main()

Model Counting

Perform Weighted Model Counting on CNF file

#!/usr/bin/env python3
from pathlib import Path
import math
from pysdd.sdd import SddManager, Vtree, WmcManager


here = Path(__file__).parent


def main():
    # Start from a given CNF and VTREE file
    vtree = Vtree.from_file(bytes(here / "input" / "simple.vtree"))
    sdd = SddManager.from_vtree(vtree)
    print(f"Created an SDD with {sdd.var_count()} variables")
    root = sdd.read_cnf_file(bytes(here / "input" / "simple.cnf"))
    # For DNF functions use `read_dnf_file`
    # If the vtree is not given, you can also use 'from_cnf_file`

    # Model Counting
    wmc = root.wmc(log_mode=True)
    w = wmc.propagate()
    print(f"Model count: {int(math.exp(w))}")

    # Weighted Model Counting
    lits = [None] + [sdd.literal(i) for i in range(1, sdd.var_count() + 1)]
    # Positive literal weight
    wmc.set_literal_weight(lits[1], math.log(0.5))
    # Negative literal weight
    wmc.set_literal_weight(-lits[1], math.log(0.5))
    w = wmc.propagate()
    print(f"Weighted model count: {math.exp(w)}")

    # Visualize SDD and VTREE
    print("saving sdd and vtree ... ", end="")
    with open(here / "output" / "sdd.dot", "w") as out:
        print(sdd.dot(), file=out)
    with open(here / "output" / "vtree.dot", "w") as out:
        print(vtree.dot(), file=out)
    print("done")


if __name__ == "__main__":
    main()

Perform Weighted Model Counting on CNF file from CLI

Given a DIMACS file test.cnf

p cnf 2 2
c weights 0.4 0.6 0.3 0.7
-1 2 0
1 -2 0

We can run the CLI:

$ pysdd -c test.cnf
reading cnf...
Read CNF: vars=2 clauses=2
creating initial vtree balanced
creating manager...
compiling...

compilation time         : 0.000 sec
 sdd size                : 2
 sdd node count          : 1
 sdd model count         : 2    0.000 sec
 sdd weighted model count: 0.54    0.000 sec
done

Conditioning

There are three ways to compute the weighted model count given that you observe the value of one or more literals:

  • Using the condition command
  • Using a conjunction
  • Using the weights

We will use the following example, a formula representing the disjunction of a and b:

mgr = SddManager(var_count=2)
a, b = mgr.vars
f = a | b
f.wmc(log_mode=False).propagate()

Using the condition command

If we want to know the WMC given that a is true, we can condition the SDD on a:

f_a = f.condition(a)

Now, f_a will represent the formula true. This is an efficient method to alter the sdd.

Note that conditioning is defined as an operation on the circuit, not the WMC. This is why the new SDD is simply true. This also means that the WMC on this new SDD will be 4 instead of 2 as you would expect. To get the correct model count, you have to ignore the possible values for a and thus use 4/2=2.

Using a conjunction

We can also conjoin the formula with the positive literal a:

f_a = f & a

Now, f_a will represent the formula a. This method is more expensive since it optimizes a formula instead of replacing a literal.

Using the weights

If you need to condition on multiple possible value assignments, it is not useful to create a new SDD for every assignment. In this case, you can alter the weights for WMC and iterate over all required value assignments:

wmc = f.wmc(log_mode=False)
wmc.set_literal_weight(a, 1)   # Set the required value for literal a to 1
wmc.set_literal_weight(-a, 0)  # Set the complement to 0
wmc.propagate()

For literal a the three options are weight(a,-a)=(1,1) for no conditioning, weight(a,-a)=(1,0) for a is true, and weight(a,-a)=(0,1) for a is false.

Command Line: pysdd-cli.py

Weighted Model Counting on CNF file

Given a DIMACS formatted CNF, examples/input/simple.cnf:

c weights 0.5 0.5 0.5 0.5 0.5 0.5 0.5 0.5 0.5 0.5 0.5 0.5
p cnf 6 3
1 4 0
-1 2 5 0
-1 -2 3 6 0

You can use the pysdd program to perform SDD compilation and weighted model counting:

$ pysdd -c examples/input/simple.cnf -W output.vtree -R output.sdd
reading cnf...
Read CNF: vars=6 clauses=3
creating initial vtree balanced
creating manager...
compiling...

compilation time         : 0.001 sec
 sdd size                : 9
 sdd node count          : 4
 sdd model count         : 36    0.000 sec
 sdd weighted model count: 0.5625    0.000 sec
saving compiled sdd ...done
saving vtree ...done
done

The resulting SDD is:

c ids of sdd nodes start at 0
c sdd nodes appear bottom-up, children before parents
c
c file syntax:
c sdd count-of-sdd-nodes
c F id-of-false-sdd-node
c T id-of-true-sdd-node
c L id-of-literal-sdd-node id-of-vtree literal
c D id-of-decomposition-sdd-node id-of-vtree number-of-elements {id-of-prime id-of-sub}*
c
sdd 15
L 1 0 1
L 4 4 2
L 5 6 -3
L 6 4 -2
F 7
D 3 5 2 4 5 6 7
L 8 10 6
L 9 8 5
L 11 6 3
D 10 5 2 4 11 6 7
T 12
D 2 7 3 3 8 6 9 10 12
L 13 0 -1
L 14 2 4
D 0 1 2 1 2 13 14

And the resulting vtree is:

c ids of vtree nodes start at 0
c ids of variables start at 1
c vtree nodes appear bottom-up, children before parents
c
c file syntax:
c vtree number-of-nodes-in-vtree
c L id-of-leaf-vtree-node id-of-variable
c I id-of-internal-vtree-node id-of-left-child id-of-right-child
c
vtree 11
L 0 1
L 2 4
L 4 2
L 6 3
I 5 4 6
I 3 2 5
L 8 5
L 10 6
I 9 8 10
I 7 3 9
I 1 0 7

SddManager

class pysdd.sdd.SddManager(long var_count=1, bool auto_gc_and_minimize=False, Vtree vtree=None)

Creates a new SDD manager, either given a vtree or using a balanced vtree over the given number of variables.

Parameters:
  • var_count – Number of variables
  • auto_gc_and_minimize – Automatic garbage collection Automatic garbage collection and automatic SDD minimization are activated in the created manager when auto gc and minimize is not 0.
  • vtree – The manager copies the input vtree. Any manipulations performed by the manager are done on its own copy, and does not affect the input vtree.

The creation and manipulation of SDDs are maintained by an SDD manager. The use of an SDD manager is analogous to the use of managers in OBDD packages such as CUDD [10]. For a discussion on the design and implementation of such systems, see [7].

To declare an SDD manager, one provides an initial vtree. By declaring an initial vtree, we also declare an initial number of variables. See the section on creating vtrees, for a few ways to specify an initial vtree.

Note that variables are referred to by an index. If there are n variables in an SDD manager, then the variables are referred to as 1, … , n. Literals are referred to by signed indices. For example, given the i-th variable, we refer to its positive literal by i and its negative literal by −i.

add_var_after

Let v be the vtree leaf node labeled with variable target var. A new leaf node labeled with variable n + 1 is created and made a right sibling of leaf v.

add_var_after_last

Let v be the rightmost leaf node in the vtree. A new leaf node labeled with variable n + 1 is created and made a right sibling of leaf v.

add_var_after_lca

Let v be the smallest vtree which contains the variables of literals, where count is the number of literals. A new leaf node labeled with variable n + 1 is created and made a right sibling of v.

add_var_before

Let v be the vtree leaf node labeled with variable target var. A new leaf node labeled with variable n + 1 is created and made a left sibling of leaf v.

add_var_before_first

Let v be the leftmost leaf node in the vtree. A new leaf node labeled with variable n + 1 is created and made a left sibling of leaf v.

add_var_before_lca

Let v be the smallest vtree which contains the variables of literals, where count is the number of literals. A new leaf node labeled with variable n + 1 is created and made a left sibling of v.

apply

Returns the result of combining two SDDs, where op can be CONJOIN (0) or DISJOIN (1).

auto_gc_and_minimize_off

Deactivates automatic garbage collection and automatic SDD minimization.

auto_gc_and_minimize_on

Activates automatic garbage collection and automatic SDD minimization.

condition

Returns the result of conditioning an SDD on a literal, where a literal is a positive or negative integer.

conjoin

Returns the result of applying the corresponding Boolean operation on the given SDDs.

copy

Returns a new SDDManager, while copying the vtree and the SDD nodes of this manager. After this operation, the given list of nodes will contain the corresponding nodes in the new manager. :param nodes: A list of SddNodes to copy. :return: The new SDDManager

count

Returns the node count of all SDD nodes in the manager.

dead_count

Returns the node count of all dead SDD nodes in the manager.

dead_size

Returns the size of all dead SDD nodes in the manager.

disjoin

Returns the result of applying the corresponding Boolean operation on the given SDDs.

dot

SDD for the given node, formatted for use with Graphviz dot.

dot_shared

Shared SDD, formatted for use with Graphviz dot.

exists

Returns the result of existentially (universally) quantifying out a variable from an SDD.

exists_multiple

Returns the result of existentially quantifying out a set of variables from an SDD.

This function is expected to be more efficient than existentially quantifying out variables one at a time. The array exists map specifies the variables to be existentially quantified out. The length of exists map is expected to be n + 1, where n is the number of variables in the manager. exists map[i] should be 1 if variable i is to be quantified out; otherwise, exists map[i] should be 0. exists map[0] is unused.

exists_multiple_static

This is the same as sdd exists multiple, except that SDD minimization is never performed when quantifying out variables.

This can be more efficient than deactivating automatic SDD minimization and calling sdd exists multiple.

A model of an SDD is a truth assignment of the SDD variables which also satisfies the SDD. The cardinality of a truth assignment is the number of variables assigned the value true. An SDD may not mention all variables in the SDD manager. An SDD model can be converted into a global model by including the missing variables, while setting their values arbitrarily.

false

Returns an SDD representing the function false.

fnf_to_sdd
forall

Returns the result of existentially (universally) quantifying out a variable from an SDD.

from_cnf_file

Create an SDD from the given CNF file.

from_cnf_string

Create an SDD from the given CNF string.

from_dnf_file

Create an SDD from the given DNF file.

from_dnf_string

Create an SDD from the given DNF string.

from_fnf

Create an SDD from the given DNF file.

from_vtree

Creates a new SDD manager, given a vtree.

The manager copies the input vtree. Any manipulations performed by the manager are done on its own copy, and does not affect the input vtree.

garbage_collect

Performs a global garbage collection: Claims all dead SDD nodes in the manager.

get_vars
global_minimize_cardinality

Returns the SDD whose models are the minimum-cardinality global models of the given SDD (i.e., with respect to the manager variables).

global_model_count

Returns the global model count of an SDD (i.e., with respect to the manager variables).

init_vtree_size_limit

Declares the size s of current SDD for vtree as the reference size for the relative size limit l.

That is, a rotation or swap operation will fail if the SDD size grows to larger than s × l.

is_auto_gc_and_minimize_on

Is automatic garbage collection and automatic SDD minimization activated?

is_prevent_transformation_on

Are transformations prevented when self.is_auto_gc_and_minimize_on()=True?

is_var_used

Returns 1 if var is referenced by a decision SDD node (dead or alive); returns 0 otherwise.

Parameters:var – Literal (number)
l

Short for literal(lit)

lca_of_literals

Returns the smallest vtree which contains the variables of literals, where count is the number of literals.

If we view the variable of each literal as a leaf vtree node, the function will then return the lowest common ancestor (lca) of these leaf nodes.

literal

Returns an SDD representing a literal.

Returns an SDD representing a literal. The variable literal is of the form ±i, where i is an index of a variable, which ranges from 1 to the number of variables in the manager. If literal is positive, then the SDD representing the positive literal of the i-th variable is returned. If literal is negative, then the SDD representing the negative literal is returned.

Parameters:lit – Literal (integer number)
live_count

Returns the node count of all live SDD nodes in the manager.

live_size

Returns the size of all live SDD nodes in the manager.

minimize

Performs global garbage collection and then tries to minimize the size of a manager’s SDD.

This function calls sdd vtree search on the manager’s vtree.

To allow for a timeout, this function can be interrupted by the keyboard interrupt (SIGINT).

minimize_cardinality

Returns the SDD whose models are the minimum-cardinality models of the given SDD (i.e. with respect to the SDD variables).

minimize_limited
minimum_cardinality

Returns the minimum-cardinality of an SDD.

The smallest cardinality attained by any of its models. The minimum-cardinality of an SDD is the same whether or not we consider the global models of the SDD.

model_count

Returns the model count of an SDD (i.e., with respect to the SDD variables).

move_var_after

Let v be the vtree leaf node labeled with variable target var. The leaf node labeled with variable var is moved to become a right sibling of leaf v.

move_var_after_last

Let v be the rightmost leaf node in the vtree. The leaf node labeled with variable var is moved to become a right sibling of leaf v.

move_var_before

Let v be the vtree leaf node labeled with variable target var. The leaf node labeled with variable var is moved to become a left sibling of leaf v.

move_var_before_first

Let v be the leftmost leaf node in the vtree. The leaf node labeled with variable var is moved to become a left sibling of leaf v.

negate

Returns the result of applying the corresponding Boolean operation on the given SDDs.

print_stdout
read_cnf_file

Replace the SDD by an SDD representing the theory in the given CNF file.

read_dnf_file

Replace the SDD by an SDD representing the theory in the given DNF file.

read_sdd_file

Reads an SDD from file.

The read SDD is guaranteed to be equivalent to the one in the file, but may have a different structure depending on the current vtree of the manager. SDD minimization will not be performed when reading an SDD from file, even if auto SDD minimization is active.

remove_var_added_last

Let v be the vtree leaf node with the variable that was added last to the vtree. This leaf is removed from the vtree.

rename_variables

Returns an SDD which is obtained by renaming variables in the SDD node. The array variable_map has size n+1, where n is the number of variables in the manager. A variable i, 1 <= i <= n, that appears in the given SDD is renamed into variable variable_map[i] (variable_map[0] is not used).

root

root: object

save

Saves an SDD to file.

Typically, one also saves the corresponding vtree to file. This allows one to read the SDD back using the same vtree.

save_as_dot

Saves an SDD to file, formatted for use with Graphviz dot.

set_options
set_prevent_transformation

Prevent transformations when prevent=True and self.is_auto_gc_and_minimize_on()=True

set_vtree_apply_time_limit

Set the time limits for the vtree search algorithm.

A vtree operation is either a rotation or a swap. Times are in seconds and correspond to CPU time. Default values, in order, are 180, 60, 30, and 10 seconds.

set_vtree_cartesian_product_limit

Sets the absolute size limit on the size of a cartesian product for right rotation and swap operations.

Default value is 8, 192.

set_vtree_fragment_time_limit

Set the time limits for the vtree search algorithm.

A vtree operation is either a rotation or a swap. Times are in seconds and correspond to CPU time. Default values, in order, are 180, 60, 30, and 10 seconds.

set_vtree_operation_memory_limit

Sets the relative memory limit for rotation and swap operations. Default value is 3.0.

set_vtree_operation_size_limit

Sets the relative size limit for rotation and swap operations.

Default value is 1.2. A size limit l is relative to the size s of an SDD for a given vtree (s is called the reference size). Hence, using this size limit requires calling the following functions to set and update the reference size s, otherwise the behavior is not defined.

set_vtree_operation_time_limit

Set the time limits for the vtree search algorithm.

A vtree operation is either a rotation or a swap. Times are in seconds and correspond to CPU time. Default values, in order, are 180, 60, 30, and 10 seconds.

set_vtree_search_convergence_threshold
set_vtree_search_time_limit

Set the time limits for the vtree search algorithm.

A vtree operation is either a rotation or a swap. Times are in seconds and correspond to CPU time. Default values, in order, are 180, 60, 30, and 10 seconds.

shared_save_as_dot

Saves the SDD of the manager’s vtree (a shared SDD), formatted for use with Graphviz dot.

size

Returns the size of all SDD nodes in the manager.

true

Returns an SDD representing the function true.

update_vtree_size_limit

Updates the reference size for relative size limits.

It is preferrable to invoke this function, as it is more efficent than the function sdd manager init vtree size limit as it does not directly recompute the size of vtree.

var_count

Returns the number of SDD variables currently associated with the manager.

var_order

Return an array var order (whose length will be equal the number of variables in the manager) with the left-to-right variable ordering of the manager’s vtree.

vtree
vtree_copy
vtree_minimize

Performs local garbage collection on vtree and then tries to minimize the size of the SDD of vtree by searching for a different vtree. Returns the root of the resulting vtree.

vtree_of_var

Returns the leaf node of a manager’s vtree, which is associated with var.

SddNode

class pysdd.sdd.SddNode
bit
condition
conjoin
copy

Returns a copy of an SDD, with respect to a new manager dest manager.

The destination manager, and the manager associated with the SDD to be copied, must have copies of the same vtree.

count

Returns the node count of an SDD (rooted at node).

deref

Dereferences an SDD node if it is not a terminal node.

Returns the node. The number of dereferences to a node cannot be larger than the number of its references (except for terminal SDD nodes, for which referencing and dereferencing has no effect).

disjoin
dot
elements

Returns an array containing the elements of an SDD node.

Returns:A list of pairs [(prime, sub)]

Internal working: If the node has m elements, the array will be of size 2m, with primes appearing at locations 0, 2, … , 2m − 2 and their corresponding subs appearing at locations 1, 3, … , 2m − 1. Assumes that sdd node is decision(node) returns 1. Moreover, the returned array should not be freed.

equiv
garbage_collected

Returns true if the SDD node with the given ID has been garbage collected; returns false otherwise.

This function may be helpful for debugging.

global_model_count
id

Unique id of the SDD node.

Every SDD node has an ID. When an SDD node is garbage collected, its structure is not freed but inserted into a gc-list. Moreover, this structure may be reused later by another, newly created SDD node, which will have its own new ID.

Returns:id
is_decision

The node is a decision node.

A functions that is useful for navigating the structure of an SDD (i.e., visiting all its nodes).

is_false

The node is a node representing false.

A functions that is useful for navigating the structure of an SDD (i.e., visiting all its nodes).

is_literal

The node is a literal.

A functions that is useful for navigating the structure of an SDD (i.e., visiting all its nodes).

is_true

The node is a node representing true.

A functions that is useful for navigating the structure of an SDD (i.e., visiting all its nodes).

literal

Returns the signed integer (i.e., variable index or the negation of a variable index) of an SDD node representing a literal. Assumes that sdd node is literal(node) returns 1.

model_count
models

A generator for the models of an SDD.

negate
node_size

Returns the size of an SDD node (the number of its elements).

Recall that the size is zero for terminal nodes (i.e., non-decision nodes).

print_ptr
ref

References an SDD node if it is not a terminal node.

Returns the node.

ref_count

Returns the reference count of an SDD node.

The reference count of a terminal SDD is 0 (terminal SDDs are always live).

save
save_as_dot
set_bit
size

Returns the size of an SDD (rooted at node).

vtree

Returns the vtree of an SDD node.

vtree2

Returns the vtree of an SDD node.

vtree_next
wmc

Create a WmcManager to perform Weighted Model Counting with this node as root.

Parameters:log_mode – Perform the computations in log mode or not (default = True)

Fnf

class pysdd.sdd.Fnf
from_cnf_file
from_dnf_file
read_cnf
read_dnf

Vtree

class pysdd.sdd.Vtree(var_count=None, var_order=None, vtree_type='balanced', filename=None, is_X_var=None)

Returns a vtree over a given number of variables.

Parameters:
  • var_count – Number of variables
  • vtree_type – The type of a vtree may be “right” (right linear), “left” (left linear), “vertical”, “balanced”, or “random”.
  • var_order – The left-to-right variable ordering is given in array var_order. The contents of array var_order must be a permutation of the integers from 1 to var count.
  • is_X_var – The constrained variables X, specified as an array of size var_count+1. For variables i where 1 =< i =< var_count, if is_X_var[i] is 1 then i is an element of X, and if it is 0 then i is not an element of X.
  • filename – The name of the file from which to create a vtree.
Returns:

A vtree
count

Returns the node count (live+dead) of all SDD nodes in the vtree.

Returns:count
count_at

Returns the node count of all SDD nodes normalized for a vtree node (the root where this Vtree points at).

For example, Vtree.size(vtree) returns the sum of Vtree.size_at(v) where v ranges over all nodes of vtree.

Returns:size
dead_count

Returns the node count (dead only) of all SDD nodes in the vtree.

Returns:count
dead_count_at
dead_size

Returns the size (dead only) of all SDD nodes in the vtree.

Returns:size
dead_size_at
dot

Vtree to Graphiv dot string.

from_file

Create Vtree from file.

get_sdd_nodes

List of SDD nodes normalized for vtree.

Only two sdd nodes for leaf vtrees: first is positive literal, second is negative literal.

Parameters:manager – SddManager associated with this Vtree
Returns:List of SddNodes
get_sdd_rootnodes

List of SDD nodes that are a root for the shared SDD.

Parameters:manager – SddManager associated with this Vtree
Returns:List of SddNodes
init_vtree_size_limit

Declares the size s of current SDD for vtree as the reference size for the relative size limit l.

That is, a rotation or swap operation will fail if the SDD size grows to larger than s × l.

is_leaf

Returns 1 if vtree is a leaf node, and 0 otherwise.

is_ref

is_ref: ‘bool’

is_sub

Returns 1 if vtree1 is a sub-vtree of vtree2 and 0 otherwise.

lca

Returns the lowest common ancestor (lca) of vtree nodes vtree1 and vtree2, assuming that root is a common ancestor of these two nodes.

left

Returns the left child of a vtree node (returns NULL if the vtree is a leaf node).

live_count

Returns the node count (live only) of all SDD nodes in the vtree.

Returns:count
live_count_at
live_size

Returns the size (live only) of all SDD nodes in the vtree.

Returns:size
live_size_at
location

Returns the location of the pointer to the vtree root.

This location can be used to access the new root of the vtree, which may have changed due to rotating some of the vtree nodes.

minimize

Performs local garbage collection on vtree and then tries to minimize the size of the SDD of vtree by searching for a different vtree. Returns the root of the resulting vtree.

new_with_X_constrained

Returns an X-constrained vtree over a given number of variables (var_count).

Parameters:
  • var_count – Number of variables
  • is_X_var – The constrained variables X, specified as an array of size var_count+1. For variables i where 1 =< i =< var_count, if is_X_var[i] is 1 then i is an element of X, and if it is 0 then i is not an element of X.
  • vtree_type – The type of a vtree may be “right” (right linear), “left” (left linear), “vertical”,

“balanced”, or “random”. :return: an X-constrained vTree

new_with_var_order

Returns a vtree over a given number of variables (var_count), whose left-to-right variable ordering is given in array var_order.

Parameters:
  • var_count – Number of variables
  • var_order – The left-to-right variable ordering. The contents of the array must be a permutation of the integers from 1 to var count.
  • vtree_type – The type of a vtree may be “right” (right linear), “left” (left linear), “vertical”,

“balanced”, or “random” :return: a vtree ordered according to var_order

parent

Returns the parent of a vtree node (return NULL if the vtree is a root node).

position

Returns the position of a given vtree node in the vtree inorder.

Position indices start at 0.

read

Reads a vtree from file.

right

Returns the right child of a vtree node (returns NULL if the vtree is a leaf node).

root
rotate_left

Rotates a vtree node left, given time and size limits.

Time and size limits, among others, are enforced when limited is set to 1; if limited is set to 0, limits are deactivated. Returns 1 if the operation succeeds and 0 otherwise (i.e., limits exceeded). This operation assumes no dead SDD nodes inside or above vtree and does not introduce any new dead SDD nodes.

rotate_right

Rotates a vtree node right, given time, size and cartesian-product limits.

Time and size limits, among others, are enforced when limited is set to 1; if limited is set to 0, limits are deactivated. Returns 1 if the operation succeeds and 0 otherwise (i.e., limits exceeded). This operation assumes no dead SDD nodes inside or above vtree and does not introduce any new dead SDD nodes.

save

Saves a vtree to file.

save_as_dot
size

Returns the size (live+dead) of all SDD nodes in the vtree.

Returns:size
size_at

Returns the size of all SDD nodes normalized for a vtree node (the root where this Vtree points at).

For example, Vtree.size(vtree) returns the sum of Vtree.size_at(v) where v ranges over all nodes of vtree.

Returns:size
swap

Swaps the children of a vtree node, given time, size and cartesian-product limits.

Time and size limits, among others, are enforced when limited is set to 1; if limited is set to 0, limits are deactivated. Returns 1 if the operation succeeds and 0 otherwise (i.e., limits exceeded). This operation assumes no dead SDD nodes inside or above vtree and does not introduce any new dead SDD nodes.

A size limit is interpreted using a context which consists of two elements. First, a vtree v which is used to define the live SDD nodes whose size is to be constrained by the limit. Second, an initial size s to be used as a reference point when measuring the amount of size increase. That is, a limit l will constrain the size of live SDD nodes in vtree v to <= l * s.

var

Returns the variable associated with a vtree node.

If the vtree node is a leaf, and returns 0 otherwise.

Returns:variable
var_count

Returns the number of variables contained in the vtree.

WmcManager

class pysdd.sdd.WmcManager(SddNode node, bool log_mode=1)

Creates a WMC manager for the SDD rooted at node and initializes literal weights.

When log mode =6 0, all computations done by the manager will be in natural log-space. Literal weights are initialized to 0 in log-mode and to 1 otherwise. A number of functions are given below for passing values to, or recovering values from, a WMC manager. In log-mode, all these values are in natural logs. Finally, a WMC manager may become invalid if garbage collection or SDD minimization takes place.

Note: To avoid invalidating a WMC manager, the user should refrain from performing the SDD operations like queries and transformations when auto garbage collection and SDD minimization is active. For this reason, the WMCManager will set the prevent_transformation flag on the SDDManager. This prevents transformations on the SDDManager when auto_gc_and_minize is on. When the WMCManager is not used anymore, Sddmanager.set_prevent_transformations(prevent=False) can be executed to re-allow transformations.

Background:

Weighted model counting (WMC) is performed with respect to a given SDD and literal weights, and is based on the following definitions:

  • The weight of a variable instantiation is the product of weights assigned to its literals.
  • The weighted model count of the SDD is the sum of weights attained by its models. Here, a model is an instantiation (of all variables in the manager) that satisfies the SDD.
  • The weighted model count of a literal is the sum of weights attained by its models that are also models of the given SDD.
  • The probability of a literal is the ratio of its weighted model count over the one for the given SDD.

To facilitate the computation of weighted model counts with respect to changing literal weights, a WMC manager is created for the given SDD. This manager stores the weights of literals, allowing one to change them, and to recompute the corresponding weighted model count each time the weights change.

literal_derivative

Returns the partial derivative of the weighted model count with respect to the weight of literal.

The result returned by this function is meaningful only after having called wmc propagate.

literal_pr

Returns the probability of literal.

The result returned by this function is meaningful only after having called wmc propagate.

literal_weight

Returns the weight of a literal.

node

node: pysdd.sdd.SddNode

one_weight

Returns 0 for log-mode and 1 otherwise.

propagate

Returns the weighted model count of the SDD underlying the WMC manager (using the current literal weights).

This function should be called each time the weights of literals are changed.

set_literal_weight

Set weight of literal.

Sets the weight of a literal in the given WMC manager (should pass the natural log of the weight in log-mode).

This is a slow function, to set one or more literal weights fast use set_literal_weights_from_array.

set_literal_weights_from_array

Set all literal weights.

Expects an array of size <nb_literals>*2 which represents literals [-3, -2, -1, 1, 2, 3]

zero_weight

Returns -inf for log-mode and 0 otherwise.

Indices and tables