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()