`zsdd`: Zero-suppressed and Subsumed Decision Diagrams for SAT Solving

[SSoelvsten]

Yi Lin, Lucas M. Tabajara and Moshe Y. Vardi are using ZDDs in the context of CNF formulas. Each clause of the given formula is represented by a single path in the ZDD. Here, any "don't care" node would represent that there are two clauses with and without a literal - the one without represents a clause that subsumes another.

Applying Decision Diagrams Reduction Rules

1. We create a new zsdd class (zero-suppressed subsumed decision diagram)

   • This has the same functions (and semantics) of ZDDs but where the "don't care" nodes are removed (similar to BDDs).

   • We can only provide a "conversion" from zsdd to zdd (see below).

   • Compared to the ZDD strategies, we need to skip recursion in more cases (when we see, that we are creating a "don't care" node). So, we slightly change each policy to also skip obvious "don't care" nodes. We can either (a) add a decorator on each policy which might be slow or (b) template the if-statement inside of each policy.

     Alternatively, we may use the reduction rules in the policy to move it back into the main algorithms?

2. The user may toggle whether to also remove "don't care" nodes. This does not change the size of intermediate output, though.

3. We add a zdd_cnf_subsumed(const __zdd &A) function that removes all don't care nodes in a ZDD.

   • [ ] If A is already reduced (and contains don't care nodes):
     • Return the input, if there are no don't care nodes.
     • Otherwise, transpose the graph and do the same as in the unreduced case.
   • [ ] If A contains an unreduced diagram:
     • Return the reduce using a special combined policy This does not fix the problem of intermediate output, though.

I would favour (1) .

Clause Distribution

The following is pseudocode taken directly from the modified CUDD artifact provided with the paper ZDD Boolean Synthesis by Yi Lin, Lucas M. Tabajara, and Moshe Y. Vardi. This is one of the key operations in their paper, since it allows one to substitute a variable for an entire clause (i.e. distribute this clause over all other variables inside of it)

zdd_clausedistribution(A,B):
  # base cases
  if A == Ø or B == Ø: return Ø
  if A == {Ø}: return B
  if B == {Ø}: return A

  # ensure A is lowest (i.e. this is symmetric)
  if A.var > B.var: return zdd_clausedistribution(B,A)

  # primary
  if |A.var - B.var| <= 1:
    # A.var and B.var represent the same variable x
    if A.var == B.var:
      if A.var is odd: return product_xn_xn(A,B)

      A = filter_tautologies(A)
      B = filter_tautologies(B)

      if A == Ø or B == Ø: return Ø
      if A == {Ø}: return B
      if B == {Ø}: return A

      if A.low.var == A.var+1:
        return product_xpxn_xpxn(A,B)
      if B.low.var == B.var+1:
        return product_xp_xpxn(A,B)
      else:
        return product_xp_xp(A,B)
    else:
      if A.low.var == A.var+1:
        return product_xpxn_xn(A,B)
      else:
        return product_xp_xn(A,B)
  else:
    # A.var and B.var represent to different variables
    A = filter_tautologies(A)

    if A == Ø: return Ø
    if A == {Ø}: return B

    if A.low.var == A.var+1:
      return product_xpxn_D(A,B)
    else:
      return product_x_D(A,B)

Notice, how the above really is an and of the two ZDDs, i.e. an intersection. The primary difference from zdd_intsec is the (quite local) two-level logic: the existence and non-existence of x_i and x_i-1 in A is paired with everything in B.

The zdd_filtertautologies(...) function removes clauses that include pairs of x and ~x literals, since such a clause is trivially satisfiable. This is a local (top-down) check of the "distance" between the variable of the current node and its child.

The functions product_* all take care of varying logic within a two-level window (for the literal x and ~x). They then call recursively further to the above main operation.

product_xpxn_D(A,B)
  f0g0 = zdd_clausedistribution(A.low.low, B)
  f0g1 = zdd_clausedistribution(A.low.high, B)
  f0    = (A.var+1, f0g0, f0g1)
  # A.high.var > A.var+1 because of filter_tautologies
  f1    = zdd_clausedistribution(A.high, B)
  return (A.var, f0, f1)

This essentially is a single top-down sweep. Yes, the way in which recursion goes and how products are made is slightly more complicated, but this already fits into Adiar today. The only thing is, that the policy may need to specify a payload to be placed with each recursion, such that it can forward some context through one or more levels.