TDDs

Overview of TDDs

Tree Decision Diagrams is a new datastructure for representing Boolean functions:

Special form of structured d-DNNF,
Tractable NEGATION, APPLY, CONDITIONING.
CANONICAL form:
- Minimal
- Can be computed from any TDD.
- Natural theoretical description.

$OBDD < TDD < SDD$

TDDs improves the tractability of OBDDs without sacrificing much.

Definition by example

Fix a vtree shape (variables at the leaves).

Input nodes: labeled by literals (constants allowed under strict conditions, see later).

A node: list of pairs of nodes from the children bags. Here, it computes $(x_1 \wedge x_2) \vee (\neg x_1 \wedge \neg x_2)$ that is $x_1 \oplus x_2 \oplus 1$ .

Another node computing $(x_1 \wedge \neg x_2) \vee (\neg x_1 \wedge x_2)$ that is $x_1 \oplus x_2$

Nodes in each bag! One output node in the root. Here it computes $(x_1 \oplus x_2 \oplus x_3 \oplus x_4) \vee ((x_1 \oplus x_2) \wedge (x_3 \oplus x_4))$

Model $\neg x_1, \neg x_2, x_3, \neg x_4$ of $(x_1 \oplus x_2 \oplus x_3 \oplus x_4) \vee ((x_1 \oplus x_2) \wedge (x_3 \oplus x_4))$

$\neg x_1, \neg x_2, \neg x_3, \neg x_4$ is not a model of $(x_1 \oplus x_2 \oplus x_3 \oplus x_4) \vee ((x_1 \oplus x_2) \wedge (x_3 \oplus x_4))$

Non deterministic TDD (nTDD): only a rigid normal form of smooth structured DNNF.

Determinism (TDD)

Determinism: Each pair of sibling nodes can be the input of at most one node.

Same node can be used twice, as long as it is used with another sibling.

For each assignment of variables and every bag $t$ , at most one node in bag $t$ is satisfied.

Negation

For each vtree node $t$ , add a $t$ -node containing all missing pairs; bottom up!

Bottom up: also add missing pairs with red nodes below!

Red nodes accept the rejected assignments at each level.

Root red node computes the negation (new output).

Complexity: $O(\#vars \cdot w^2)$ where $w$ is the width, ie, maximum number of nodes in a bag.

Canonicity and Minimization

Twins contraction

Two nodes $N_1,N_2$ are twins if they have the same siblings for every parent node.

Same sibling for this parent.

But not for this one: these two nodes are not twins.

Same sibling for this parent.

And for this one. They are twins!

We can merge them. This does not change the function computed.

Minimization

Theorem.

Iteratively merging twins until no twins remains converges to a canonical and minimal TDD computing the same function.

In particular: TDDs can be minimized in polynomial time.

Next slides: why is the result canonical and minimal?

Subfunctions

Let $f : 2^X \rightarrow \{0,1\}$ and $Y \subseteq X$ . Subfunctions of $f$ on $Y$ :

$subfunctions(f,Y) = \{ f[\tau] \mid \tau \in 2^{X \setminus Y}, f[\tau] \neq \bot\}.$

Example:
- $EVEN_4(x_1,x_2,0,0) = EVEN_4(x_1,x_2,1,1) = EVEN_2(x_1,x_2)$
- $EVEN_4(x_1,x_2,1,0) = EVEN_4(x_1,x_2,0,1) = ODD_2(x_1,x_2)$
- $EVEN_4$ has two subfunctions on $\{x_1,x_2\}$ .

Subfunctions and canonicity

Lower bound:

For two models $\tau_1, \tau_2$ of node $N$ , $f[\tau_1] = f[\tau_2]$ .

$\tau_1$ and $\tau_2$ define the same subfunction!

At least $\#subfunctions(f,X_t)$ nodes in bag $t$ for each $t$

Upper bound:

If one bag $t$ has size $> \#subfunctions(f,X_t)$ , the TDD must contain one pair of twins.

Iteratively contracting twins converges to a canonical minimal TDD!

Bottom-up compilation

def cnf2tdd(F: cnf, T: vtree):
    D = TDD(1, T)
    for c in F:
        Dc = TDD(c, T)
        D.apply(Dc)
        D.minimize()
    return D

For a CNF $F = C_1 \wedge \dots \wedge C_m$ with $n$ variables:

Let $W_i =$ width of $F_i = C_1 \wedge \dots \wedge C_i$ .
Runs in time $O(nm \cdot (\max W_i))$
$O(2^k \cdot nm)$ for CNF of incidence tw $k$ !
Complexity follows by just analysing the number of subfunctions!

Conclusion

The slides you missed

Learning TDD

Angluin-style learning algorithm.

Build the canonical TDD of size $S$ of a Boolean function with $O(S)$ equivalence queries to the oracle.

Compiling constraints

Bottom up algorithm with constraints represented by TDDs over the same vtree.

FPT compilation with bounded incidence treewidth:

Parity constraints
Cardinality constraints etc.

Existential and Universal Projection

Given a TDD $C$ of width $w$ and $Y \subseteq X$ .

We can construct a TDD computing $\exists Y. C$ and $\forall Y. C$ of width at most $2^w$ !

Applications to QBF solving!

Future work

Work in progress: Certified TDD using the CPOG framework.
Open questions on lower bounds:
1. TDD vs Canonical SDD: are they comparable?
  - Canonical SDD $\not <$ TDD is known.
  - Do we have (TDD $<$ Canonical SDD) or (TDD $\not <$ Canonical SDD)?
2. TDD vs OBDD
  - Currently known separation is quasipolynomial.
  - Do we have quasipolynomial simulation? Exponential separation?

And in practice? TiDiDi compiler! Stay tuned with Guy!

TDD — Tree Decision Diagrams