Decision diagrams have steadily become more prominent in the field of combinatorial optimization, being able to outperform the state-of-the-art in e.g. scheduling problems[13]. They have proven even more capable with the introduction of methods such as decision diagram-based Branch & Bound. Often, layer-based binary decision diagram (BDD) encodings are used to encode the problem domain, where a layered structure determines the decisions and decision variables. Recently, state-based multivalued decision diagram (MDD) encodings have also been considered. These do not rely on a layered structure, as instead, each state makes its decisions on the variables independently of other states. This allows for more flexible decision-making as states do not have to compromise with other states on the decisions they make.

This thesis compares these newer state-based MDDs with the commonly used layer-based BDDs, while also introducing and evaluating heuristics for the state-based MDDs. These heuristics include a new beam restriction heuristic that limits the branching factor of the MDDs, a dynamic variable ordering strategy adapted for the new state-based context, and a new local bound for the maximum independent set problem (MISP).

The experiments of this thesis show that the state-based MDDs generally outperform the layer-based BDDs in both runtime and search tree size. Only for some instances with low graph densities, the state-based MDDs were slower. This is resolved with the newly introduced beam restrictions, which can significantly lower the runtime. This speedup is also shown for the graph coloring problem, although the application of the beam restrictions is not as straightforward there as with the MISP. Both the dynamic variable ordering and the new local bound for the MISP show great promise in increasing the efficiency of the search, but are both held back by the additional overhead they introduce. Fortunately, these two techniques can share the added overhead while gaining the combined benefits, resulting in great performance for the MISP when both methods are used together.

The formalization of mathematics has become increasingly popular in recent years. Formalization refers to the expression of mathematical definitions and proofs within a precisely defined system of rules, allowing software programs to verify their correctness. This thesis formalizes Schwartz functions using the interactive theorem prover Lean, which provides automation and feedback during the construction of definitions and arguments. Due to their smoothness and rapid decay at infinity, the space of Schwartz functions forms a natural setting for the Fourier transform. While Lean's library already contains an abstract formalization of Schwartz functions, this thesis presents a more concrete, coordinate-based approach that aligns more closely with standard mathematical textbooks. The knowledge gained throughout this thesis can support future formalizations of results in distribution theory, a domain that is still underdeveloped in Lean.

This thesis considers the thin-film equation ∂_tu = −∂_x (|u|ⁿ∂³x u) with respect to time t ≥ 0 and one dimensional space x ∈ R where n > 0. A special case of the thin-film equation is when the initial condition is u₀(x,0) = cδ(x). A solution with this initial condition is called a source type solution. A source type solution describes how a viscous droplet spreads over a solid flat surface with volume c > 0. Source type solutions are expected to have a self-similar form with u(x,t) = t^{-α}f (μ), μ = xt^{-α} and α = 1/(n+4) which reduces the equation into an ordinary boundary-value problem (|f (μ)|ⁿ f ′′′(μ))′ = α(μf (μ))′ with μf (μ)→0 as μ→±∞ and
∫_{-∞}^{∞} f (μ)dμ = c. A solution of this boundary-value problem is called a self-similar solution. This thesis presents a detailed discussion of the paper in 1992 by Bernis, Peletier & Williams on the existence and uniqueness of self-similar solutions to the thin-film equation together with its qualitative properties. Here, existence will be proven by using a shooting method. Additionally, the thin-film equation will be derived from the Navier-Stokes equations using a lubrication approximation. Furthermore, a numerical construction of the
self-similar solution is presented to visualize its behavior. The results demonstrate that the solution exhibits key qualitative features such as compact support and conservation of mass.

This thesis explores the Kakeya conjecture for n=2, which states that every subset of Rⁿ containing a unit line segment in every direction has Minkowski dimension n. To tackle this problem we explore what the Minkowski dimension is, and use the Kakeya maximal operator. We start by stating the idea of a Kakeya needle set. We construct a sequence of these sets with arbitrarily small measure, followed by looking at Kakeya sets, which can even have measure equal to zero. We derive a proof of the Kakeya conjecture using the Kakeya maximal operator conjecture and its dual form, where we also prove all necessary implications. Resulting in a complete proof for n=2 with respect to the Minkowski dimension.

Phylogenetic networks generalize evolutionary trees and are commonly used to represent evolutionary relationships between species that undergo reticulate evolutionary processes such as hybridization, recombination and lateral gene transfer. In this thesis all quarnets, networks on four species, of a network are assumed to be known. We prove that each recoverable undirected or semi-directed binary level-2 phylogenetic network without redundant biconnected components is encoded by its set of quarnets, meaning that the network is uniquely determined by its quarnets. Furthermore, two decomposition theorems for undirected and semi-directed binary phylogenetic networks are presented. These decomposition theorems are proved for undirected binary phylogenetic networks for all levels and for semi-directed binary phylogenetic networks that are at most level-2.