# Dictionary Encoding Based on Tagged Sentential Decision Diagrams
## 2 Preliminaries  
Throughout this paper, we use lowercase letters (e.g., \(x_{1},x_{2}\)) for variables and bold uppercase letters (e.g., \(\mathbf{X},\mathbf{Y}\)) for sets of variables. For a variable \(x\), we use \(\overline{x}\) to denote the negation of \(x\). A literal is a variable or a negated one. A truth assignment over \(\mathbf{X}\) is the mapping \(\sigma:\mathbf{X}\mapsto\{0,1\}\). We let \(\Sigma_{\mathbf{X}}\) be the set of truth assignments over \(\mathbf{X}\). We say \(f\) is a Boolean function over \(\mathbf{X}\), which is the mapping \(\Sigma_{\mathbf{X}}\mapsto\{0,1\}\). We use \(\mathbf{1}\) (resp. \(\mathbf{0}\)) for the Boolean function that maps all assignments to \(1\) (resp. \(0\)). Let \(\mathbf{X}\) and \(\mathbf{Y}\) be two disjoint and non-empty sets of variables. We use \(f\) to denote a Boolean function and use \(f(\mathbf{X})\) to denote a Boolean function over the variable set \(\mathbf{X}\). We say the set \(\{(f_{1}^{p}(\mathbf{X}),f_{1}^{s}(\mathbf{Y})),\cdots,(f_{n}^{p}(\mathbf{X}),f_{n}^{s}(\mathbf{Y}))\}\) is an \((\mathbf{X},\mathbf{Y})\)-_decomposition_ of a Boolean function \(f(\mathbf{X},\mathbf{Y})\) iff \(f=(f_{1}^{p}(\mathbf{X})\wedge f_{1}^{s}(\mathbf{Y}))\vee\cdots\vee(f_{n}^{p}( \mathbf{X})\wedge f_{n}^{s}(\mathbf{Y}))\), where every \(f_{i}^{p}(\mathbf{X})\) (resp. \(f_{i}^{s}(\mathbf{Y})\)) is a Boolean function over \(\mathbf{X}\) (resp. \(\mathbf{Y}\)). A decomposition is compressed iff \(f_{i}^{s}\
eq f_{j}^{s}\) for \(i\
eq j\). An \((\mathbf{X},\mathbf{Y})\)-decomposition is called an \((\mathbf{X},\mathbf{Y})\)-partition iff (1) \(f_{i}^{p}\
eq\mathbf{0}\) for \(1\leq i\leq n\), (2) \(f_{i}^{p}\wedge f_{j}^{p}=\mathbf{0}\) for \(i\
eq j\), and (3) \(f_{i}^{p}\vee\cdots\lor f_{n}^{p}=\mathbf{1}\). A vtree is a full binary tree whose leaves are labeled by variables, and we use \(\mathbf{T}\) to denote a vtree node. Then, we use \(\mathbf{T}_{l}\) to denote the left subtree of \(\mathbf{T}\), while \(\mathbf{T}_{r}\) denotes the right subtree of \(\mathbf{T}\). The set of variables appearing in the leaves of \(\mathbf{T}\) is denoted by \(v(\mathbf{T})\). In addition, there is a special leaf node labeled by \(0\), which can be considered a child of any vtree node, and \(v(0)=\emptyset\). The notation \(\mathbf{T}^{1}\preccurlyeq\mathbf{T}^{2}\) denotes that \(\mathbf{T}^{1}\) is a subtree of \(\mathbf{T}^{2}\). In order to unify the definition, we use a tuple to denote a decision diagram in this paper and give the following definition. **Definition 1**. : _A decision diagram is a tuple \((\mathbf{T}^{1},\mathbf{T}^{2},\alpha)\) s.t. \(\mathbf{T}^{2}\preccurlyeq\mathbf{T}^{1}\), which is recursively defined as follows:_  
* \(\alpha\) _is a terminal node labeled by one of four symbols:_ \(\mathbf{1}\)_,_ \(\mathbf{0}\)_,_ \(\mathbf{\varepsilon}\)_, or_ \(\bar{\mathbf{\varepsilon}}\)_;_
* \(\alpha\) _is a decomposition node_ \(\{(p_{1},s_{1}),\cdots,(p_{n},s_{n})\}\) _satisfying the following:_
* _Each_ \(p_{i}\) _is a decision diagram_ \((\mathbf{T}^{3},\mathbf{T}^{4},\beta)\)_, where_ \(\mathbf{T}^{4}\preccurlyeq\mathbf{T}^{3}\prec\mathbf{T}^{2}\)_;_
* _Each_ \(s_{i}\) _is a decision diagram_ \((\mathbf{T}^{5},\mathbf{T}^{6},\gamma)\)_, where_ \(\mathbf{T}^{6}\preccurlyeq\mathbf{T}^{5}\prec\mathbf{T}^{2}\)_._  
The size of \(\alpha\) is denoted by \(|\alpha|\), and \(|\alpha|=0\) when \(\alpha\) is a terminal node and \(|\alpha|=n\) when \(\alpha=\{(p_{1},s_{1}),\cdots,(p_{n},s_{n})\}\). We use \(\langle(\mathbf{T}^{1},\mathbf{T}^{2},\alpha)\rangle\) to denote the Boolean function that this decision diagram represents. Then, we give the definition of the syntax of decision diagrams. **Definition 2**. : _Let \(\mathbf{T}^{1}\) and \(\mathbf{T}^{2}\) be two vtrees, and let \(\mathbf{T}^{2}\) be a subtree of \(\mathbf{T}^{1}\).