# Minimization Strategies

**ddSMT** implements two fundamentally different strategies for input
minimization (**ddmin** and **hierarchical**), which can be combined
into the best of both worlds, strategy **hybrid**.

Strategy **ddmin** implements a variant of the minimization strategy from
[Zel99], and is the direct successor of what the original **ddSMT**
from [NB13] implemented: it tries to perform mutations on multiple
S-expressions in the input in parallel.
Strategy **hierarchical** performs a simple breadth-first traversal through the
input and applies mutations to every S-expression, one mutation at a time
(similar to what is presented as “hierarchical delta-debugging” in
[BB09]).
Strategy **hybrid** is the **default** strategy of **ddSMT**.
It first applies **ddmin** until a fixed point is reached, and then calls
strategy **hierarchical** on the simplified input.

For a more in-depth analysis of these minimization strategies, see [KNP21].

## The **ddmin** Strategy

Strategy **ddmin** tries to perform simplifications on multiple S-expressions
in the input in parallel.
The algorithm below shows the main loop of **ddmin** in pseudo code.
For each active mutator `M`

, the algorithm first collects all
S-expressions in the input that can be simplified by `M`

(Line 4).
Simplifications are applied and checked in a fashion similar to the original
ddmin algorithm [ZH02]:

the set of S-expressions

`sexprs`

is partitioned into subsets of size`size`

each S-expression

`e`

from`subset`

is substituted in the current`input`

(Line 7) with a simplification suggested by mutator`M`

the resulting simplified input candidate is then checked if it still triggers the original behavior from the golden run (Line 8)

Once all subsets of a given size are checked, `sexprs`

is updated based
on the current input and partitioned into smaller subsets.
As soon as all subsets of size 1 were checked, these steps are repeated
with the next mutator.
This loop is run until the input cannot be further simplified.

**ddmin** applies mutators in two stages. The first stage targets
top-level S-expressions (e.g., specific kinds of SMT-LIB commands) until a
fixed point to aggressively simplify the input before applying more expensive
mutators in the second stage.

## The **hierarchical** Strategy

The main loop of the **hierarchical** strategy (as shown in pseudo code below)
performs a simple breadth-first traversal
of the S-expressions in the input, and applies all enabled mutators
to every S-expression.
Once a simplification is found (Line 7), all pending checks for the current
S-expression are aborted and the breadth-first traversal continues with the
simplified S-expression `sexpr`

(Line 9).
This process is repeated until further simplifications are found.

The main simplification loop (Line 3) is applied multiple times, with varying
sets of mutators.
In the initial stages, **hierarchical** aims for aggressive minimization
using only a small set of selected mutators, in the next-to-last stage it
employs all but a few mutators that usually only have cosmetic impact, and in
the last stage it includes all mutators.

Breadth-first traversal yields significantly better results than a depth-first traversal, most probably since it tends to favor simplifications on larger subtrees of the input.

## The **hybrid** Strategy

Strategy **hybrid** is the **default** strategy of **ddSMT**.
It combines strategies **ddmin** and **hierarchical** in a sequential
portfolio manner for a best of both worlds.

Strategy **hybrid** first applies **ddmin** until a fixed point is reached, and
then calls strategy **hierarchical** on the simplified input.
This order of strategies is due to our observation that **ddmin**
is usually faster in simplifying input, while **hierarchical** often
yields smaller inputs.