Rule Rewriting Revisited: A Fresh Look at Static Filtering for Datalog and ASP

An atom $\underset{¯}{a}$ is an expression $p(𝒕)$ with $p\in 𝐏$, $𝒕$ a list of terms, and $\text{ar}(p)=|𝒕|$. A (Datalog) rule $\rho$ is a formula $H\leftarrow B$, where the head $H$ is an atom, the body $B$ is a conjunction of atoms, and all variables are implicitly universally quantified. We require that all variables in $H$ also occur in $B$ (safety). Conjunctions of atoms may be treated as sets of atoms. A (Datalog) program $P$ is a finite set of rules. A predicate $p$ is an EDB atom in $P$ if it only occurs in rule bodies, and an IDB atom if it occurs in some rule head.²²2These terms originate from extensional/intentional database.

A fact for predicate $p$ is an atom $p(𝒄)$ with $𝒄\subseteq 𝐂$. A database $𝒟$ for a program $P$ is a potentially infinite set of facts for EDB predicates of $P$. We allow $𝒟$ to be infinite, so as to accommodate conceptually infinite built-in relations, such as $\le$. Practical systems typically evaluate such built-ins on demand and syntactically ensure that infinite built-ins do not lead to infinite derivations, e.g., by requiring that variables in built-ins also occur in body atoms with finite predicates. Such concerns are unimportant to our results, so we can unify (given) input facts and (computed) built-in relations.

The (unique) model $ℳ$ for program $P$ and database $𝒟$ is the least set of facts such that (1) $𝒟\subseteq ℳ$, and (2) for every rule $\rho \in P$ with variables $𝒙$, and every mapping $\sigma :𝒙\to 𝐂$, if $\sigma (B)\subseteq ℳ$ then $\sigma (H)\subseteq ℳ$. If $\sigma (B)\subseteq ℳ$, we also call $\sigma$ a match of $\rho$ on $ℳ$. Models can be equivalently defined through iterated rule applications, proof trees, or as least models of $P$ viewed as a first-order logic theory [1].

For a rule $H\leftarrow B$ with variables $𝒙$, a mapping $\sigma :𝒙\to 𝐂$ is applicable to a database $𝒟$ if $B\sigma \subseteq 𝒟$ and $H\sigma ⊈𝒟$. A set of facts $𝒟$ is closed under a program $P$, written $𝒟\vDash P$, if there is no $\rho \in P$ with an applicable mapping $\sigma$. For a predicate $p$, let $p^{𝒟}=\{𝒄\mid p(𝒄)\in 𝒟\}$ denote the tuples of $p$-facts in $𝒟$.

To simplify presentation, we require that rules contain only variables, no constants, and that atoms in rules do not contain repeated variables. This normal form can be established by defining auxiliary EDB predicates ${(\text{␣}\stackrel{\cdot }{=}\text{␣})}^{𝒟}=\{⟨𝚌,𝚌⟩\mid 𝚌\in 𝐂\}$ and ${(\text{␣}\stackrel{\cdot }{=}𝚍)}^{𝒟}=\{𝚍\}$ for every constant $𝚍\in 𝐂$. Now every occurrence of $𝚍\in 𝐂$ in a rule is replaced by a fresh variable $x$, and the atom $x\stackrel{\cdot }{=}𝚍$ is added to the rule body. Similarly, every non-first occurrence of a variable $x$ in a body atom is replaced by a fresh variable $x^{\prime }$, and the atom $x\stackrel{\cdot }{=}{x}^{\prime }$ is added to the rule body. Similar normalisations can be used for any built-in function that reasoners might support, e.g., arithmetic functions as in a rule $p(x+y)\leftarrow q(x,y)$ can be rewritten as $p(z)\leftarrow q(x,y)\wedge z\stackrel{\cdot }{=}x+y$ with ${(\text{␣}\stackrel{\cdot }{=}\text{␣}+\text{␣})}^{𝒟}=\{⟨𝚕,𝚖,𝚗⟩\in {𝐂}^3\mid 𝚕=𝚖+𝚗\}$. As before, the infinite EDB predicate is just a conceptual model for a real systems’ on-demand computation of its supported built-in functions.

Given a program $P$, we consider distinguished sets ${𝐏}_{\text{out}}\subseteq 𝐏$ of output predicates and $𝐅\subseteq 𝐏$ of filter predicates, where all filter predicates must be EDB predicates in $P$. Outputs define which inferences are of interest to users, and are supported in many reasoners, including the ones in Table 1. Filters are used in our algorithms to reduce inferences for non-output predicates, and would be defined by the reasoner implementation: they should be easy to check and highly selective. For example, the above predicates for $\stackrel{\cdot }{=}$ are good filters, whereas an EDB predicate that is stored in a large file on disk most likely is not. However, specific predicates like “$x$ is a string with letter e in third position” or pre-loaded data with fast index structures can also be suitable filters. Given a set of atoms $B$, we define $B_{𝐅}=\{p(𝒕)\in B\mid p\in 𝐅\}$ and $B_{\overline{𝐅}}=B\setminus B_{𝐅}$ as the conjunction of atoms with filter predicates and, respectively, atoms with non-filter predicates.

A rule with generalised filter expressions has the form $H\leftarrow B_{\overline{𝐅}}\wedge G_{𝐅}$ with $H$ a head atom, $B_{\overline{𝐅}}$ a conjunction of non-filter atoms, and $G_{𝐅}\in 𝐆$ a positive boolean combination of filter atoms, defined recursively:

Positive boolean combinations of body atoms are normally syntactic sugar in Datalog: we can replace any (body) disjunction $A[𝒙]\vee B[𝒚]$ over (possibly overlapping) sets of variables $𝒙$ and $𝒚$ by a fresh atom $D[𝒙\cup 𝒚]$, and add rules $D[𝒙\cup 𝒚]\leftarrow A[𝒙]$ and $D[𝒙\cup 𝒚]\leftarrow B[𝒚]$. The fresh atom $D$ avoids the exponential blow-up that would occur if we would instead create two copies of the rule, one with $A$ and one with $B$. With potentially infinite filter predicates, however, this syntactic transformation is not natural, since the auxiliary $D$ could be infinite, whereas it is easy for systems to evaluate nested expressions $G_{𝐅}$ in place. Therefore, if not otherwise stated, all programs below may include generalised filters. Their normal form is defined as for Datalog.

For a given arity $k>0$, let ${𝐍}_k=\{\mathrm{𝟏},\mathrm{\dots },𝒌\}$ be a set of $k$ positional markers. A filter atom (for arity $k$) is an expression $\underset{¯}{f}=p({𝒎}_{\mathrm{𝟏}},\mathrm{\dots },{𝒎}_{\mathbf{\ell }})$ where $p\in 𝐅$ with $\mathrm{\ell }=\text{ar}(p)$ and ${𝒎}_{𝒊}\in {𝐍}_k$ for $i=1,\mathrm{\dots },\mathrm{\ell }$. The semantics of $\underset{¯}{f}$ is the relation ${\underset{¯}{f}}^{𝒟}=\{𝒄\in {𝐂}^k\mid ⟨c_{m_1},\mathrm{\dots },c_{m_{\mathrm{\ell }}}⟩\in p^{𝒟}\}$. Let $𝐅[k]$ be the set of all filter atoms of arity $k$ over $𝐅$. The filter formulas ${ℱ}_k$ are the positive boolean formulas over $𝐅[k]$:

Their semantics is defined as expected: ${\top }^{𝒟}={𝐂}^k$, ${\perp }^{𝒟}=\mathrm{\varnothing }$, ${(F\wedge G)}^{𝒟}=F^{𝒟}\cap G^{𝒟}$, and ${(F\vee G)}^{𝒟}=F^{𝒟}\cup G^{𝒟}$. Given filter formulas $F,G\in {ℱ}_k$, we write $F\vDash G$ if $F^{𝒟}\subseteq G^{𝒟}$, and $F\equiv G$ if $F\vDash G$ and $G\vDash F$. We can assume that $\perp$ and $\top$ are only used at the root level, using the usual simplifications: $(\perp \wedge F)\mapsto \perp$, $(\top \wedge F)\mapsto F$, $(\perp \vee F)\mapsto F$, and $(\top \vee F)\mapsto \top$ (and their commutated versions). A filter formula is simplified if none of these rewritings applies to it.

Example 2 might use filter predicates $\text{␣}\stackrel{\cdot }{=}𝚊$, $\text{␣}\le \mathrm{\hspace{0.17em}5}$, and $\text{␣}\stackrel{\cdot }{=}\text{␣}+1$. Since filter formulas do not allow constants, we assume distinct predicates for every pattern of constant use. Implementations generally decide which filters to consider – those that occur syntactically are required, but others can be added.

For every IDB predicate $p\in 𝐏$, we seek a filter formula $\text{flt}(p)\in {ℱ}_{\text{ar}(p)}$, such that we only need to derive facts $p(𝒄)$ if $𝒄\in \text{flt}{(p)}^{𝒟}$. To obtain an algorithm, some operations have to be concretely implemented for the chosen filters $𝐅$ and every $k\ge 1$:

1. 1.

   It must be possible to decide $F\vDash G$ for any $F,G\in {ℱ}_k$.

2. 2.

   There is a canonical representation function $\text{rep}:{ℱ}_k\to {ℱ}_k$, such that $\text{rep}(F)\equiv F$, and $F\equiv G$ implies $\text{rep}(F)=\text{rep}(G)$, for all $F,G\in {ℱ}_k$.

For an atom $p(𝒙)$ with arity $\text{ar}(p)=k$, the mapping ${\iota }_{p(𝒙)}:𝒊\mapsto x_i$ maps the positional markers $\mathrm{𝟏},\mathrm{\dots },𝒌$ to $𝒙$. We extend ${\iota }_{p(𝒙)}$ to filter formulas $F$, i.e., we obtain ${\iota }_{p(𝒙)}(F)$ by replacing each positional marker $𝒊$ with ${\iota }_{p(𝒙)}(𝒊)=x_i$. For $r(x,y,n)$ of rule (5) and $F=\mathrm{𝟑}\le 5$, e.g., we get ${\iota }_{r(x,y,n)}(F)={\iota }_{r(x,y,n)}(\mathrm{𝟑}\le 5)=n\le 5$.

Algorithm 1 describes the iterative computation of optimised filters. Line L2 initialises filters to $\top$ for output predicates (“compute all facts”), and to $\perp$ for all others. The formulas are then generalised by looping over all rules (L4) and their non-filter body atoms (L5). Matches to a rule can be restricted to those that satisfy both the head predicate’s filter $\text{flt}(h)$ and the rule’s own filter expression $G_{𝐅}$, which are combined into a filter formula $G\in {ℱ}_{|\text{var}(\rho )|}$ (L6); we map $\text{flt}(h)$ to the variables used in the rule. To find the strongest filter formula $M$ for body atom $b(𝒚)$, we take a conjunction of all filters $F\in {ℱ}_{\text{ar}(b)}$ that follow from $G$ when mapping $F$ to variables $𝒚$ as used in $b(𝒚)$ (L7). Finally, we generalise the current filter for $b$ by including the new $M$ disjunctively, and taking the canonical representation (L8).

Algorithm 1 is correct in the sense that rule applications can be safely restricted to applying rules only when the conclusion $p(𝒄)$ satisfies the computed filter formula $\text{flt}(p)$, as there is no risk of changing derivations for outputs. However, adding body atoms for $\text{flt}(p)$ to all rules is often redundant. The next definition characterises choices for equivalent filter conditions.

The conditions of Definition 4 ensure that admissible filters are equivalent to the canonically extended body filter $F_{+}$ under the assumption that body atoms are also restricted to their computed filters $F_{-}$. We obtain the following.

Note that $F_{+}$ as given in Definition 4 is always admissible, but there can be much simpler expressions. Algorithm 2 shows a practical way to find good admissible filters, which would also find the rewriting of Example 6. An occurrence $o$ of an atom in $\psi$ refers to a single position in $\psi$ where some atom is found (even if the same atom occurs more than once), and $\psi [o\mapsto \top ]$ denotes the result of replacing this occurrence by $\top$. Each iteration in line L12 preserves admissibility of $\psi$, and the algorithm terminates after linearly many iterations.

While the concrete performance impact of the rewriting depends on $P$ and $𝒟$, static filtering is guaranteed to only reduce but never increase the number of logical entailments. The next result is a direct consequence of the proof of Theorem 5, where we showed that ${ℳ}^{\prime }=\{q(𝒅)\in ℳ\mid 𝒅\in \text{flt}{(q)}^{𝒟}\}\cup 𝒟$:

In particular, every derivation (proof tree) over $𝒟$ and $P^{\prime }$ corresponds to a analogous derivation over $𝒟$ and $P$, and the bottom-up computation of ${ℳ}^{\prime }$ requires at most as many rule applications as the bottom-up computation of $ℳ$. The additional cost associated with the use of $P^{\prime }$ is limited to the cost of checking, for each rule match, if the rewritten filters rather than the original filters are satisfied. This cost can be controlled by system designers through the choice of filter predicates to push. The potential savings, on the other hand, can be in the order of $|ℳ|$.

The fact that static filtering preserves the structure of rules, programs, and derivations also improves understandability by human users and compatibility with other optimisations, be it logical (e.g., magic sets) or operational (e.g., join-order optimisation). The rewriting is even idempotent, i.e., already optimised programs will not be modified further when applying static filtering again. None of these advantages is common to all logic program optimisation methods, a prominent counterexample being magic sets.

Finally, we investigate the impact of (tractable) static filtering for reasoning over real-world data. We implement conjunctive approximate static filtering (CASF) for linear orders and instantiations of the rules of Example 20 for all natural numbers in a program $P$. Moreover, we treat EDB predicates as filter predicates. We rewrite programs for transitive closure over Wikidata properties via CASF, and we compare the runtime of the original programs with the rewritten ones as well as the runtime for static filtering. In particular, we show that

1. 1.

   static filtering can improve the performance of modern rule systems by orders of magnitude,

2. 2.

   the simplifications in Section 5 are general enough to obtain these improvements, and

3. 3.

   the time necessary for applying tractable static filtering is negligible.

As a typical examples for recursive programs, we use programs for computing the transitive closure of a predicate, and we add an output predicate out and a filter $x\stackrel{\cdot }{=}𝚊$ for a constant $𝚊$. We use a template for transitive closure (see Figure 1), which we instantiated for different EDB predicates $p(x,y)$. We extract these predicates from Wikidata properties (see Figure 2). As rule systems, we considered Soufflé v2.5 [20], Nemo v0.8.1 [18], Clingo v5.8.0 [13], and DLV v2.1.2 [2]. We have adopted the programs and inputs to the capabilities of the rule systems: Soufflé and Nemo received facts as CSV files, while Gringo and DLV received them as a list of facts. We applied a timeout at 5min. Our measurements are performed on a regular notebook (Linux; AMD Ryzen 7 PRO 5850U; 16 GiB RAM).

Figure 3 shows the runtimes for Programs 1 instantiated with the properties of Table 2. For each property, we run each system with the original program and the rewritten one. In all cases, the rewritten programs require significantly less time – note the log-scale of the plot. For the properties where the systems could finish for the original program, static filtering provides a speed-up in the order of magnitude (from $6.6$ times for P1203 and Clingo to $30$ times for P2652 and DLV). Moreover, static filtering enables all systems to finish for huge properties with up to $1,000,000$ facts within seconds, while all system reached the timeout for the original program there. Finally, we observe that static filtering can be done in a few milliseconds, and it is independent of the number of facts for the underlying property.

Our experiments show that (tractable) static filtering can improve the performance of rule systems significantly. However, evaluating a static optimisation method empirically has its limitations. Static optimization, by design, works on inputs that are not manually optimized yet. While such programs are common in practice, there is no grounds for assuming anything about how common this is. Existing public program collections are not representative here either, since most of these published programs have been carefully optimised by experts – exactly the type of manual work that static optimisations try to automate.

A negated atom is an expression $\mathrm{𝑛𝑜𝑡}p(𝒕)$ with $p\in 𝐏$ and $|𝒕|=\text{ar}(p)$. A normal rule $\rho$ is a formula $H\leftarrow B\wedge B^{-}$, where the head $H$ is an atom, $B$ is a conjunction of atoms, and $B^{-}$ is a conjunction of negated non-filter atoms, such that every $v\in \text{var}(\rho )$ occurs in some atom $p(𝒙)\in B$ (safety). Negated filter atoms are not needed: we can express them by introducing fresh filter predicates that are interpreted by the complemented relation. Analogously to Datalog, a normal rule with generalised filter expressions has the form $H\leftarrow B_{\overline{𝐅}}\wedge B_{\overline{𝐅}}^{-}\wedge G_{𝐅}$ with $H$ a head atom, $B_{\overline{𝐅}}$ a conjunction of non-filter atoms, and $G_{𝐅}\in 𝐆$ a positive boolean combination of filter atoms. In this section, all rules and programs may include negated atoms and generalised filters (we omit normal). The normal form without repeated variables per (negated or non-negated) atom is defined as for Datalog.

For a program $P$ and database $𝒟$, let $\text{gr}(P)=\{\rho \sigma \mid \rho \in P,\sigma :𝐕\to 𝐂\}$ be its grounding. For a set of facts $𝒜$, the Datalog program $\text{gr}{(P)}^{𝒜}=\{H\leftarrow B\mid H\leftarrow B\wedge B^{-}\in \text{gr}(P),B^{-}\cap 𝒜=\mathrm{\varnothing }\}$ is the reduct. $𝒜$ is a stable model of $P$ and $𝒟$ if $𝒜$ is the model of $\text{gr}{(P)}^{𝒜}$ and $𝒟$. We write $\text{sm}(P,𝒟)$ for the set of all such stable models.

Even when using stable models, we check if programs are (partly) stratified, so as to tighten some filters. Let $G_P$ be the graph with the IDB predicates of $P$ as its vertices, and, for every rule $q(𝒙)\leftarrow B_{\overline{𝐅}}\wedge B_{\overline{𝐅}}^{-}\wedge G_{𝐅}\in P$, a positive edge $p{\to }_{+}q$ for all IDBs $p$ in $B_{\overline{𝐅}}$, and a negative edge $p{\to }_{-}q$ for all IDBs $p$ in $B_{\overline{𝐅}}^{-}$. The stratifiable predicates ${𝐏}_{\text{str}}$ are the vertices $p$ of $G_P$ such that there is no cycle $C$ in $G_P$ such that $C$ a negative edge and $p$ is reachable from $C$.

Importantly, facts that do not contribute directly to the output can still have an impact on stable models. For example, consider a program $P$ with a stable model $𝒜$ that contains some $q(𝒄)\in 𝒜$; then adding a rule $p(𝒙)\leftarrow q(𝒙)\wedge \mathrm{𝑛𝑜𝑡}p(𝒙)$ for a fresh $p$ means that $𝒜$ is no longer stable. Hence, static filtering must not filter facts $p(𝒄)$ relevant to some $\mathrm{𝑛𝑜𝑡}p(𝒙)$.

We therefore define more general initial filters for negated predicates. For a rule $\rho =h(𝒙)\leftarrow B_{\overline{𝐅}}\wedge B_{\overline{𝐅}}^{-}\wedge G_{𝐅}$ with $b(𝒚)\in B_{\overline{𝐅}}^{-}$, let $M_{b(𝒚)}=\bigwedge \{F\in {ℱ}_{\text{ar}(b)}\mid G_{𝐅}\vDash {\iota }_{b(𝒚)}(F)\}$, and let $N_{\rho }^p=\bigvee \{M_{p(𝒚)}\mid p(𝒚)\in B_{\overline{𝐅}}^{-}\}$ with $\bigvee \mathrm{\varnothing }=\perp$. To obtain a procedure for a program $P$, we can now modify Algorithm 1 so that the formulas $\text{flt}(p)$ are initialised in line L2 with

Note that $\text{flt}(p)\equiv \perp$ for $p\notin {𝐏}_{\text{str}}$ if $p$ never occurs in a negated atom. Predicates $p\notin {𝐏}_{\text{str}}$ can be initialised with $\text{rep}(\perp )$ as before, but we have to consider them in the iterative generalisation: we modify line L5 to loop over all $b(𝒚)$ with $b(𝒚)\in B_{\overline{𝐅}}$ or $\mathrm{𝑛𝑜𝑡}b(𝒚)\in B_{\overline{𝐅}}^{-}$ for IDB predicate $b$.

Our remaining definitions require only minimal adaptations. For a rule $\rho =h(𝒙)\leftarrow B_{\overline{𝐅}}\wedge B_{\overline{𝐅}}^{-}\wedge G_{𝐅}$, a filter formula $\psi$ is admissible for $\rho$ if $\psi$ is admissible for $h(𝒙)\leftarrow B_{\overline{𝐅}}\wedge G_{𝐅}$, and $h(𝒙)\leftarrow B_{\overline{𝐅}}\wedge B_{\overline{𝐅}}^{-}\wedge \psi$ is an admissible rewriting of $\rho$. An admissible rewriting of a program $P$ is a set that contains an admissible rewriting of each rule of $P$. We can use Algorithm 2 unchanged as a practical way to find good admissible filters. Our main correctness results shows visible equivalence [19] between $P$ and $P^{\prime }$:

In particular, since $\text{flt}(p)\equiv \top$ for output predicates $p$, the restrictions of $\text{sm}(P,𝒟)$ and $\text{sm}(P^{\prime },𝒟)$ to facts over output predicates coincide.

One can easily incorporate the ideas of Section 5 to obtain a tractable optimisation procedure for normal logic programs.

The filter computation of Kifer and Lozinskii [24] can be seen as a special case of our approach for a fixed choice of filter predicates (binary equalities and inequalities, possibly involving constants) and representation of filter formulas (in disjunctive normal form). Predicates such as $\text{␣}\stackrel{\cdot }{=}\text{␣}+1$ in Example 2 are not considered as filters. The significance of our generalisation is witnessed by exponential increases in complexity (Section 4), but also by the ability to introduce tractable simplifications (Section 5). The general notion of admissibility and Algorithm 2 are also new.

Kifer and Lozinskii further include a similar method to propagate projections and remove unused predicate parameters. This rewriting is simpler than filter propagation. We have nothing to add to it but note that it is particularly effective if static filtering is applied first.

Kifer and Lozinskii have already compared their special case of static filtering to existing methods including magic sets [3, 28, 29], and they have have already observed that the approaches by Walker [34] and Gardarin et al. [12] are similar, yet less general. Subsequently, Chang et al. extended the original method of Kifer and Lozinskii to programs with stratified negation, which is less general than our extension to ASP.

Constraint pushing [21, 30] considers rules with constraint atoms, with a propagation scheme similar to Algorithm 1. However, the method might not terminate, as there can be infinitely many constraint atoms.

Zaniolo et al. introduce pre-mappability (PreM) as a sufficient condition for pushing filters into recursive rules, identify some classes of PreM filters, and use such filters to rewrite recursive programs with aggregates [36]. Our Algorithm 1 can be seen as a systematic method for producing pre-mappable filters ($\text{flt}(p)$ are pre-mappable).

The FGH-rule by Wang et al. [35] defines a sufficient condition for rewriting a program using given output predicates (or queries), and our admissile rewritings satisfy this condition (which is true for any rewriting that produces the same output facts). Hence, static filtering offers a tractable method to find FGH-rule conforming rewritings.

In general, static filtering promises to work well with some rewriting techniques such as projection propagation and pre-mappability [36], and it is unlikely that it interferes negatively with static optimisations techniques, since static filtering preserves the program structure.

Magic sets [3, 28, 29] and the closely related demand transformation [31, 32] are static optimisation methods that also aim at reducing inferences by making some rule bodies more selective, and which may seem similar to static filtering on an intuitive level. However, in almost all cases, their outputs are very different from ours, for the following reasons:

1. 1.

   Static filtering preserves the number of rules and the structure of their non-filter atoms. Magic sets and demand transformation always increase the number of rules and add rules that contain partial body joins.

2. 2.

   Static filtering cannot optimise programs that do not contain filter predicates. Demand transformation can be used on purely abstract programs.

3. 3.

   Static filtering uses symbolic reasoning over filters to simplify and summarise expressions, so rewritten rules may contain new derived filters. Magic sets and demand transformation foresee no mechanism for integrating any symbolic knowledge about existing EDB predicates, so rewritten rules are always based on copies of EDB atoms that are syntactic parts of the program.

4. 4.

   Static filtering is idempotent (optimised programs are not rewritten further). The transformation by magic sets and demand transformation always changes the program, even if applied to its own output.

5. 5.

   Static filtering makes use of recursive rules for recursively generalising filter expressions. Demand transformation in turn supports rewritings of IDB predicates that are defined by recursive rules.

6. 6.

   Static filtering includes a simplification step that removes filters that have become redundant after pushing (via admissibility, Def. 4). Magic sets and demand transformation have no mechanism to detect possible simplifications.

Therefore, we do not see any general principle to obtain the benefits of static filtering from magic sets or demand transformation, even in special cases or with further adjustments. Rather, the methods are complementary and can be used together, where static filtering should go first since any reduction in body atoms can reduce the cost of the other transformation.