arXiv subjects

Steffan Christ Sølvsten

Publications and source records attributed to Steffan Christ Sølvsten.

5 recordsLinked to original sources

arXiv2026

Multi-variable Quantification of BDDs in External Memory using Nested Sweeping (Extended Paper)

Previous research on the Adiar BDD package has been successful at designing algorithms capable of handling large Binary Decision Diagrams (BDDs) stored in external memory. To do so, it uses consecutive sweeps through the BDDs to resolve computations. Yet, this approach has kept algorithms for multi-variable quantification, the relational product, and variable reordering out of its scope. In this work, we address this by introducing the nested sweeping framework. Here, multiple concurrent sweeps pass information between eachother to compute the result. We have implemented the framework in Adiar and used it to create a new external memory multi-variable quantification algorithm. Compared to conventional depth-first implementations, Adiar with nested sweeping is able to solve more instances of our benchmarks and/or solve them faster.

cs.DS↗

arXiv2026

Efficient Binary Decision Diagram Manipulation in External Memory

We follow up on the idea of Lars Arge to rephrase the Reduce and Apply procedures of Binary Decision Diagrams (BDDs) as iterative I/O-efficient algorithms. We identify multiple avenues to simplify and improve the performance of his proposed algorithms. Furthermore, we extend the technique to other common BDD operations, many of which are not derivable using Apply operations alone, and we provide asymptotic improvements for the procedures that can be derived using Apply. These algorithms are implemented in a new BDD package, named Adiar. We see very promising results when comparing the performance of Adiar with conventional BDD packages that use recursive depth-first algorithms. For instances larger than 8.2 GiB, our algorithms, in parts using the disk, are 1.47 to 3.69 times slower compared to CUDD and Sylvan, exclusively using main memory. Yet, our proposed techniques are able to obtain this performance at a fraction of the main memory needed by conventional BDD packages to function. Furthermore, with Adiar we are able to manipulate BDDs that outgrow main memory and so surpass the limits of other BDD packages.

cs.DS↗

arXiv2025

Predicting Memory Demands of BDD Operations using Maximum Graph Cuts (Extended Paper)

The BDD package Adiar manipulates Binary Decision Diagrams (BDDs) in external memory. This enables handling big BDDs, but the performance suffers when dealing with moderate-sized BDDs. This is mostly due to initializing expensive external memory data structures, even if their contents can fit entirely inside internal memory. The contents of these auxiliary data structures always correspond to a graph cut in an input or output BDD. Specifically, these cuts respect the levels of the BDD. We formalise the shape of these cuts and prove sound upper bounds on their maximum size for each BDD operation. We have implemented these upper bounds within Adiar. With these bounds, it can predict whether a faster internal memory variant of the auxiliary data structures can be used. In practice, this improves Adiar's running time across the board. Specifically for the moderate-sized BDDs, this results in an average reduction of the computation time by 86.1% (median of 89.7%). In some cases, the difference is even 99.9\%. When checking equivalence of hardware circuits from the EPFL Benchmark Suite, for one of the instances the time was decreased by 52 hours.

cs.DS↗

arXiv2025

Symbolic Model Checking in External Memory

We extend the external memory BDD package Adiar with support for monotone variable substitution. Doing so, it now supports the relational product operation at the heart of symbolic model checking. We also identify additional avenues for merging variable substitution fully and the conjunction operation partially inside the relational product's existential quantification step. For smaller BDDs, these additional ideas improve the running of Adiar for model checking tasks up to 47%. For larger instances, the computation time is mostly unaffected as it is dominated by the existential quantification. Adiar's relational product is about one order of magnitude slower than conventional depth-first BDD implementations. Yet, its I/O-efficiency allows its running time to be virtually independent of the amount of internal memory. This allows it to compute on BDDs with much less internal memory and potentially to solve model checking tasks beyond the reach of conventional implementations. Compared to the only other external memory BDD package, CAL, Adiar is several orders of magnitude faster when computing on larger instances.

cs.DS↗

arXiv2020

Existential Theory of the Reals Completeness of Stationary Nash Equilibria in Perfect Information Stochastic Games

We show that the problem of deciding whether in a multi-player perfect information recursive game (i.e. a stochastic game with terminal rewards) there exists a stationary Nash equilibrium ensuring each player a certain payoff is Existential Theory of the Reals complete. Our result holds for acyclic games, where a Nash equilibrium may be computed efficiently by backward induction, and even for deterministic acyclic games with non-negative terminal rewards. We further extend our results to the existence of Nash equilibria where a single player is surely winning. Combining our result with known gadget games without any stationary Nash equilibrium, we obtain that for cyclic games, just deciding existence of any stationary Nash equilibrium is Existential Theory of the Reals complete. This holds for reach-a-set games, stay-in-a-set games, and for deterministic recursive games.

cs.GT↗