Sylvan 2.0

[trolando]

I want to get started on Sylvan 2.0 with an opportunity to redesign parts of the API.

Some currently planned action points:

• Add more benchmarks, including benchmarks that would benefit from automatic variable reordering
  • Update https://github.com/ssoelvsten/bdd-benchmark/ to work with Sylvan 2.0
  • Port Adam Walker's solver (https://adamwalker.github.io/The-Reactive-Synthesis-Competition/, https://github.com/adamwalker/syntcomp, for safety games using BDDs. This makes heavy use of automated ordering.
    ⚠️ Actually, Andrej already did that for his MSc. thesis, I just need to copy it? Sweet! (Still some work to do...)
    ⚠️ Benchmark input files to be found at https://github.com/SYNTCOMP/benchmarks/tree/master/aiger
  • Figure out what happened to the old LTSmin benchmarks set... we only have a few models in the repository now!
    ⚠️ I have a lot more models now but some are very big, much too big for this repository. Better to move benchmarks out of the repository rather than in...
• Integrate Lace 2.0 (this would hopefully make the code look cleaner)
  🌟 Appears to be neutral wrt performance (more benchmarks are needed)
• Get rid of the "sylvan_granularity" (it doesn't seem to have impact and it clutters the code)
  🌟 Appears to be neutral wrt performance (more benchmarks are needed)
• Fix a long-standing race condition in the operation cache (affected modern Apple ARM chips)
  🌟 Appears to be neutral wrt performance (more benchmarks are needed)
• Determine the system's cache line size automatically when configuring CMake
• Set up GitHub Actions to be functional again
• Include testing "make install" in GitHub Actions
• Fix a strange bug in zdd_isop that causes the zdd_isop_random test to fail.
  🌟 Turns out it was just an array overflow bug in the test...
• Make the C++ wrapper optional to build (via CMake setting)
• Do something more useful with sylvan_config.h, maybe as CMake options?
• Clean up the API, perform some renaming
  • Restructure header files, move public headers to an include directory
  • Renamed the header files, they don't need to all start with sylvan_
  • Revised the CMake scripts to ensure that building and installing should work perfectly
  • Rename llmsset to nodes to prepare for different ways to handle the nodes.
  • Rename "_t" structures to follow standards more
  • Probably rename a lot of the sylvan_ operations to mtbdd_ and bdd_ operations?
  • Consistently use ldd and LDD instead of lddmc and MDD
  • Change all functions that return a DD to expect a result pointer as the first parameter -- This is fairly important to eliminate the complexity of preventing garbage collection problems when running multiple Sylvan operations from different threads
  • Functions like sylvan_makenode should be fully internal, not safe to use from outside Lace threads.
  • Do not typically return the internal "level" of a DD node, rather, when returning for example the variable of the DD root, rather return an ithvar (DD with just that variable) instead.
• Experiment with replacing the hash table by a structure that only looks at parents of nodes (similar to Ruddy)
  • Check what happens if the hash table doesn't rehash, but just follows the linear probe sequence...
  • One version with a simple linked list, with two arrays: "first" (first parent) and "next" (next parent). When empty, use cas with a magic value to claim, then make the actual node, and release. A wait-free alternative could first make the actual node, and then use cas to update.
  • Other version with a trie based on the hash of the node, with two arrays: "first" and "next", but for next we store two values, "next0" and "next1". Same update mechanisms to consider as in the first version.
• Consider using just malloc and realloc rather than mmap since they use mmap internally anyway for large allocations
  ⚠️ Only if we actually use realloc to grow. Otherwise Sylvan startup times are huge!!
• Ensure that there are never pointers into the nodes table, only indices even inside internal methods.
• Experiment with different versions of the operations cache, specifically an RCU cache instead of seqlock, and thread-local operation caches. Daniel Basgöze implemented a version that has its own cache-garbage-collection, storing indices to the cache in an array (which does add one level of indirection, mitigated by storing part of the hash in each bucket), and having a third array to record potential free-able slots in the data array.
  • I'm not quite sure if a different operation cache is better, or whether there could be a better policy for when to resize it, or metrics to see how effective the cache is
  • One option (probably bad) is thread-local operation caches, so no mutexes are needed
  • RCU version: each bucket only has a pointer to actual data (never cleared until gc, so can be safely read until gc, maybe thread-local?) Eg a fixed amount of space for new cache entries, and once full, run gc and rebalance memories?
• Consider different hash functions, although this is a low priority. One could record all the operations stored in the cache and compare histograms of different hash functions; it is likely that the CPU time is not super important due to memory accesses being the bottle neck, but the quality of the hashes might also not be extremely important for the operation cache.
• Consider different node layouts:
  • Maybe a 64 bits version, with 22 bits index (4M nodes) and 10 bits variable (1024 variables). This could be useful for cases where we just don't expect such large BDDs or where we want to smoothly transition to bigger nodes when we reach the 4M mark.
  • Maybe a 256 bits version, with a 128 bits "core" BDD node plus 2x64 bits for an edge label (see if this can be compatible with Q-Sylvan)
  • Note: the current 128 bits version has 40 bits index (1T nodes) and 24 bits variable (16M variables).
• Reconsider how external references are done, i.e., the API for adding custom references, etc. Rewrite the mark function to cope with millions of roots (in some use cases)
• Give a better way to configure "grow policies" i.e. as the table grows in size, at what point(s) do we actually want to do garbage collection? When do we increase the size of the operations cache, etc.
  • In fact, if the new nodes implementation is successful (no significant performance loss, or even improved performance) then we don't need to grow the nodes table in powers of 2! It could be any arbitrary size. See the discussion below for a potential API.
• Add fast algorithms for contains, subset, subseteq, etc.
• Implement mtbdd_subsume
• Implement mtbdd_satcount with GMP values
• Improve support for ZDD (consider what functionality is missing but critical... I had a list somewhere...)
• Integrate support for TBDD
  • Rewrite to use 40-bit indices, 14-bit variables to work with the new nodes implementation.
• Consider putting ZDD, TBDD, LDD in separate unique tables / node arrays. This would be useful for implementing sifting, because you can't do sifting if there are also non-BDD nodes in the array!
• Integrate / Reimplement dynamic variable ordering (sifting) and benchmark different tuning parameters
  • "Grouping" of variables that should always move together
  • "Barriers" to forbid moving variables beyond
• Improve documentation and website
  • Set up Doxygen and automation
  • Maintainer's guide
  • Tutorial
  • Including how to "install" (and to a custom directory)
• Better testing! Testing is very basic at the moment. Use the Unity framework, add a lot more unit tests just to ensure that things work.
• Reconsider the design of sylvan_stats, maybe allow programmatic access rather than just dumping to screen?
• In general, look at the CPU profile on benchmarks, what is dominating now?
• Rewrite wrappers for C++, Python, Rust, Java.
  • Keep the C++ wrapper in the Sylvan repository
  • For Python: update de adapter in https://github.com/tulip-control/dd
  • For Rust: https://github.com/daemontus/sylvan-sys
  • For Java: https://github.com/utwente-fmt/jsylvan (probably need a full rewrite)
• Add an option to run single-threaded with a "fake" Lace??
  ⚠️ Probably not doing this. Even with a fake Lace, Sylvan has overhead anyway with atomic operations.
• Consider some kind of support for sentential decision diagrams (http://reasoning.cs.ucla.edu/sdd/)
  ⚠️ Not for Sylvan 2.0, maybe Sylvan 2.1?
• Add more timer counters for operations, percentage of time spent in the cache operations vs just Sylvan operations

[trolando]

I also intend to review the open issues and pull requests on the Sylvan project (here and at utwente-fmt).

Any suggestions/comments, @alaarman @ssoelvsten @jacopol @daemontus @johnyf ?

[daemontus]

Hmm... thank you for the question :)

I don't think I have anything very specific on my wish list for Sylvan 2.0... it would be nice to have a slightly more detailed documentation about stuff like grow policies or some of the more advanced features/operators, but that is to some extent my "skill issue" :D

Regarding the points you mentioned:

• If you are talking about the hash table from this paper (https://repositum.tuwien.at/handle/20.500.12708/188807), the actual implementation is here (https://github.com/sybila/ruddy). Sorry for the confusion, seems that we simultaneously picked the name Ruddy and never realized there is a collision (technically, we were using it internally since the paper in 2022, but it was in a private repo, so I wouldn't expect the other author to know about that, and then we just never checked the uniqueness again after public release).
• Regarding sentential decision diagrams... it's a cool feature, but so far my experience is that it is very hard to implement completely (e.g. to the best of my knowledge, even libraries that do say they implement SDDs, like https://github.com/neuppl/rsdd, only implement a subset of the full data structure). So, like variable reordering, I do believe there are cases where SDDs could be very useful, but I'm not quite sure if the extra overhead and implementation complexity is worth pursuing (but it would be very cool!).

I'll try to add more stuff if something else comes to mind :) Good luck with the implementation!

[trolando]

I think the idea that you can do unique checking without a hash table by just checking the parents of the greatest/smallest child is quite clever. With a hash table you have to increase the size of the table when it gets full and it's also not always clear when it's full, and do you do garbage collection or not, but with just an array of nodes you can let it increase gradually until some configured point where you do the garbage collection. I can see a way to make it scalable multi-threaded, so managing the nodes becomes much easier.

So I'm certainly interested to see how it would work in Sylvan. It might also make dynamic variable reordering easier.

[trolando]

Also, https://github.com/sybila/ruddy seems to be a private repository? I can download the MSc. thesis artefacts from the repository I think.

[trolando]

@ssoelvsten from your BDD benchmarks repository, which ones would be most useful to use for Sylvan benchmarking? I'm trying to see if I want to have a few specific ones in the Sylvan repository as well.

[alaarman]

If you implement SDD, then have a look at variable-shift SDD. It seems like a minor increment which brings the compression from singly to doubly exponential in the best case. It just makes sense to reinterpret the variables depending on the path through the vtree.

[ssoelvsten]

I'm happy to see you, Tom, are just as enamoured with that hash table as I am. :D I could imagine that it's cache-efficiency works really well for multi-threading: not only does it seem that it might induce fewer memory accesses (thereby making the workers trip each other up) but there might even be less contention. Furthermore, it would likely resolve your biggest performance issue with small BDDs in a large table.

Notes on your action points:

• While there certainly could be some more fine-grained control over how the hash tables grow, there also needs to be something simpler. A good API caters to both novices, experts, and the people in-between. As in Memorycap in sylvan_set_limits #39 shows, people don't want to reverse-engineer the size of the tables from their memory limits.

• With respect to node size, the 64 bit version sounds useful but you probably need the user to supply the number of variables at initialization. While the user most often knows this number, you should also provide a sylvan_maxvar static variable that one can use when the number is unknown.

  Furthermore, Sylvan is with its 128 bits already the BDD package with the most compact node representation (maybe only Ruddy has a smaller encoding when it uses its 16-bit indices).

• I'm not entirely convinced that you gain anything from splitting the tables between different diagram types. Does it make the implementation nicer as you can add a bit more type-safety?

• For documentation, I recommend Doxygen or similar such that you don't have to keep a separate documentation synchronised. You might be able to knick some of the CMake, Doxygen, and more from Adiar's docs/ folder. Here is the CI script for recompiling it automatically.

• While Sylvan has some performance issues with a single thread, I'm not certain it is worth the implementation effort. Indeed, it makes Sylvan look worse in my papers. But, (1) I'm not likely going to publish any more Adiar papers (except maybe one of the two left on arXiv) and (2) most BDD papers within the immediate future seem to focus on multi-threaded BDD computation where you still win. So, I don't think this is going to be so much a negative in future research it is worth your effort.

• Here is Adiar's statistics struct for a reference.

• When reconsidering how external references are done, you might want to consider this issue I ran into .

A few additional action points:

• From our email exchange back in March 2024, one performance issue of Sylvan is due to the fact that it only uses a single memoisation cache. In particular, operations that can be nested, i.e. apply, should be placed in a separate table. This allows Sylvan to compute its exists and forall with a much smaller memoisation cache.

Notes on C++:

• Since C++ allows for function overloading, this makes the novice and expert interface much easier to do without compromise or making a mess. So, you might want to leave the C interface expert-only but can then instead improve the C++ interface.
• The C++ interface ought to rely much more on iterators rather than forcing the user to provide their data in a specific data structure. Furthermore, you might also want to consider coroutines and predicate functions as possible inputs. For example, see the four overloads of bdd_exists in Adiar.
• Even though C++ provides classes, you don't need to emulate an OOP-style. The C++ standard library uses snake_case and is much closer to a C-style data oriented design. Now, there are good reasons to stick with the current style - especially to ease transition from CUDD. On the other hand, switching makes it not only more similar the standard library but also to Sylvan's C interface, BuDDy, Adiar, and probably other BDD packages too.
• You may also want to take a look at Sylvan's benchmarking adapter . It contains a few conversions that arguably ought to be part of Sylvan's API.

Notes on Benchmarks:

• I would ignore the combinatorial problems, i.e. Hamiltonian Cycle, Queens, Tic-Tac-Toe, and Game of Life. These are designed for the BDD to explode quickly. But, they are not as realistic.

  I'm not entirely certain about the properties of Nils' CNF benchmark, so this leaves:

  • Apply / RelProd : Recreates the single-operation benchmark from Samuel and other's recent paper.
  • Picotrav : Recreates CUDD's Nanotrav which uses apply, not, and equality for circuit testing.
  • QBF : Uses apply, not, exists, and forall, and a few other operations to solve a QBF encoding (of 2-player games).
  • McNet : Foundations for a model checker which currently includes Reachability and Deadlock analysis and also SCC Decomposition; maybe I can get some (BSc) students to add CTL checking too.

  The last three benchmarks might also be interesting for dynamic variable reordering. Picotrav has a wide difference in performance depending on the ordering used (without reordering). If reordering is enabled, this might be even further improved.

• Instead of reimplementing these benchmarks, I personally would recommend you integrate your CI directly with them. This way you can leverage the fact that the benchmarks are a centralised place of common interest: the benchmarks will grow and bugs will be fixed.

  The repository already includes a regression script to compare performance of two branches. This works as long as there are no breaking changes. You can see an example of it in use here .

• From a documentation perspective, these benchmarks are almost too complex for your examples/ folder. If you want to redo them for documentation, then maybe hardcode the inputs. Otherwise, it drowns in non-BDD shenanigans.

[trolando]

• Regarding SDDs, I think I'll leave that for a later version, let's say Sylvan 2.1 or something. I'll read the papers and see if I can do Sylvan 2.0 in a way that won't hinder a potential SDD extension.

• Indeed, I think the different "uniqueness" mechanism and potentially the idea of delaying garbage collection a little longer might make Sylvan much faster on small tables.

• The reason for maybe splitting the tables has to do with variable reordering. Variable reordering basically is designed for BDDs, to get it to work for TBDDs or ZDDs requires different rules for doing the swaps. So if you want sifting, you have to drop ZDD/TBDDs. I am unsure whether there is a real downside to having multiple tables if we're using the new approach to ensuring nodes are unique. Another advantage.

• The single-threaded performance bugs me a bit in the sense that various papers report on the performance of Sylvan in single-thread mode, while it's explicitly designed for multi-threading and in fact takes a small performance hit with atomic operations like compare-and-swap in order to be thread-safe. Processors typically have 8 cores if not more, you have to be very cheap to buy a 6 core CPU or even less. Thus I think any comparison where Sylvan doesn't get to use the actual resources of the computer is rather unfair. Maybe I should just add an explicit warning about benchmarking on a single core rather than trying to add an option for that though, because I surely don't want to add single-threaded versions of every part of Sylvan.

• Benchmarks: I don't necessarily want to copy all benchmarks from your repository, I think I want something like I have in Lace and Oink: a bunch of small benchmarks that could also serve as examples, and that give a sufficiently representative idea of what implementation details are ideal for performance. Maybe I could leverage your repo as a subproject, then if your repo can detect that it is used as a subproject and check what targets already exist, it could decide to just build for whatever project it is included in? I was also thinking of grabbing "simply bdd solver" (solves safety games) since it heavily relies on CUDD's reordering, then have either QBF or Picotrav, and maybe I was thinking of having a simple BDD-based SAT solver too, but that may overlap with QBF already? Are qbf and picotrav doable as single-file units like I have with bddmc and lddmc? The bddmc example is a very simple state space exploration.

[ssoelvsten]

Currently, all BDD packages are imported via submodules. So using it directly as a subproject of Sylvan would create a cyclic dependency. If this somehow can be fixed, then you sure can do it that way - but at that point you may as well just provide a link to my repo or a fork of your own? Since almost all operations are done via an adapter, the use of Sylvan is quite hidden.

All benchmarks in said repo are already single-file units.

I personally do not have good experience with BDD-based SAT solvers . You can use it for a simple example, sure. But, the application is not "realistic".

[daemontus]

Ah, sorry, didn't realize the repo was not public yet. Anyway, https://github.com/sybila/ruddy should be public now :) At this point, it's just the same stuff you can download with the thesis. It still needs a bit of cleanup (e.g. a proper README and release on crates.io), but should be more usable than the artifact published with the original paper.

[trolando]

I've started work on this issue now, although I will also go on holiday pretty soon. I have created the branch sylvan-2.

[trolando]

I just thought of something: if the approach using small embedded tries instead of a hash table is sufficient (no loss of performance, hopefully an improved performance) then this makes setting "table limits" much easier.

• The "nodes storage" can be of arbitrary size, and it grows naturally. We could simply say something like "use at most 39 GB" and that would just work as a limit. So anyone telling Sylvan to use 39 GB can actually see that being used, rather than asking "why does it crash out at 16 GB"
• We can simply configure a "garbage collection when there are X nodes" and then depending on the result, set the next X, for example #nodes * 2. The nodes table grows naturally, until some maximum point that is configured.
• For resizing the operations cache, we could have a similar policy, e.g.:
  • Whenever garbage collection is done, wipe the cache and decide on the new size
  • Whenever we reach some arbitrary number of nodes (at least X), resize the hash table (no wipe needed)

So the API would look something like this:

• set_max_nodes(size_t) to set the max size of the nodes table
• set_cache_size(size_t) sets the size of the cache (power of two would save an expensive division, but perhaps we are not CPU bound anyway in 2025, so it could be any number)
• set_next_gc(size_t) to decide when garbage collection will be done (with maximum of max_nodes)
• on_nodes_size(size_t, callback)
• A post-gc hook is called with the result of garbage collection, at which point a user could do set_next_gc and set_cache_size
• A default post-gc hook would set the next gc to twice the number of nodes, and would have the cache size be that number too.

Something like this:

void post_gc(size_t node_count, size_t cache_size, size_t nodes_max)
{
    set_next_gc(node_count*2);
    set_cache_size(node_count*2 > nodes_max ? nodes_max : node_count*2);
}

I need to think a bit on how to do the "whenever we reach some arbitrary number of nodes" in a clean way, probably also just a single callback that is set and if set again is updated, so we don't get a lot of these triggers. Just two: one for doing garbage collection, and one for resizing the cache. Why not only follow garbage collection, you might ask? Well, what if we just want to let the table grow to 1GB and do garbage collection then? Then how do we determine the size of the operation cache?

We don't need to have a precise count of nodes anywhere, that would create a terrible performance hot spot. But Sylvan gives a thread a block of 512 (iirc) nodes, so when a thread runs out of 512 nodes, it uses cas on a bit array to claim the next free 512 nodes, and you could just say if X=N*512 blocks have been claimed, that's the point where we run garbage collection.

Also, I think if memory is full, rather than crash out (which you mentioned in an issue somewhere), we could just make a sylvan_outofmemory constant to return. We have sylvan_invalid (-1) so sylvan_outofmemory could be -2.

[trolando]

In the meantime I've released v1.9.0 of Sylvan which includes significant improvements to the build script, pulls in the latest Lace pre-2.0 version for better hwloc support, and contains critical fixes to the operation cache for ARM chips such as the Apple ARM processors.