Seadog optimiser

Seadog is an optimiser for tket2, that uses concepts from graph rewriting (aka graph transformation systems) to transform a graph representing a computation. The objective of the optimiser is to find a modified graph that represents a computation that is equivalent to the original input, but such that the estimated computation cost is minimal.

Seadog is the second optimiser after Badger. They both share the same API and the same objectives, but they differ in how the optimisation is performed.

Note: Badger used to work differently (and as of 31/10/25, tket2/main and all released versions still expose the old badger: hereafter old-badger and new-badger). old-badger only works by providing equivalence classes of circuits. By contrast, new-badger can support a much larger variety of rewrites using the new API that consists of Matchers and Replacers, which is shared with Seadog. Under the hood, Badger has not changed, but the expressivity of its API has significantly improved in the new version.

High level overview of how the optimisers (both badger and seadog) work

1. A quantum computation (represented as a HUGR graph) is passed to the optimiser as input
2. Possible graph rewrites that can be applied to the input are generated by tket2. Rewrites are composed of a) a left hand side (LHS)---the subgraph that has been matched; and b) a right hand side (RHS)---the new graph that should be inserted in place of the matched LHS.
   • in old-badger, rewrites were generated from a set of pattern quantum circuits and equivalence classes of circuits: given a class of quantum circuits, all pairwise equivalent, tket2 finds instances of these circuits in the input, and then generates a rewrite that replaces the matched circuit with another, equivalent, circuit
   • in new-badger and seadog, rewrites can be generated by the combination of a tket2 Matcher and a tket2 Replacer. Together, they can be used to construct a MatchReplaceRewriter object, which will use the Matcher to find rewrite LHS, and then call the Replacer to compute the corresponding RHS. Multiple MatchReplaceRewriters can be passed together to the optimiser, so that any rewrite from any of the rewriter will be considered for optimisation.
3. This is where the optimiser comes in: it must figure out which rewrites can be applied in parallel (versus which overlap and thus are mutually exclusive) and which set of rewrites lead to the best optimised computation. More than one rewriting step is typically necessary, which means the optimiser must explore the optimisation landscape by trying out multiple sets of rewrites, before choosing which one is the best.
4. After rewrites have been applied, we return to generating new rewrites at step 2, repeating steps 2 and 3 until the optimiser deems that the optimum has been found (typically, no more progress is made or a timeout is reached).

A much more detailed presentation of how Seadog works specifically can be gleaned from Chapter 5 of this thesis.

Code structure

As it is not possible (or I was not smart enough) to split a python package with bindings to Rust code into two packages, all code lives within the tket2 repo, but not (yet) on main. As of 31/10/2025, the most up-to-date branch is seadog/oct27. You may want to check if there are more recent branches/tags that following this template.

The main modules of interest to us:

• tket/src/optimiser: This contains the code for both new-badger and seadog. Both are fairly simple wrappers around a simple BacktrackingOptimiser (in `tket/src/optimiser/backtracking.rs)
• tket/src/rewrite_space: Implements RewriteSpace, a core concept specifically for the seadog optimiser. The rewrite space keeps track of all sequences of rewrites that can be applied to the input. Filling this rewrite space will all options forms the first half of the seadog optimiser, called the "exploration phase". This is a pretty simple wrapper around PersistentHugr, from the upstream hugr_persistent crate.
• tket/src/rewrite_space/max_sat.rs: Given an already explored rewrite space, this encodes all the dependencies between the rewrites in the rewrite space as a SAT problem, such that every boolean assignment that satisfies the formula is a valid choice of rewrites to apply to the input. The problem of finding the optimal computation graph that can be reached using rewrites in the rewrite space is then given by an optimisation problem over the set of satisfying boolean assignments, which can be solved (and is solved) using z3.
• hit/: A stand-alone binary that can be used to debug seadog. It's a CLI tool that tries to mimick the git interface. More specifically, the rewrite space that seadog explores can be saved to a file using the save_rewrite_space option (available both in Python and Rust). The space can then be loaded into the hit tool by running hit load <saved_rewrite_space_file> (you will need to write cargo run -p hit -- load <saved_file> unless you install the compiled binary to a location on your PATH). Have a look at hit help to see the options: briefly, hit log --all will show all rewrites in the space; hit checkout <IDs> will let you explore the state of the computation graph after having applied the IDed rewrites; hit show will print out the computation graph at the current checked out history in various formats.

How to release new versions of new-badger + seadog

See recording of handover meeting with Dan and Maria. Within this repo (tket2-seadog-wheels), there is a CI script (found at .github/workflows/build-wheels.yml) that can be run to automatically build wheels of tket2 for a particular commit/tag of tket2. Go to "Actions -> Build custom tket2 wheel -> Run workflow -> Enter SHA/tag/branch name". When completed, the compiled binaries are found under releases.

Plan to merge new-badger into main:

The following features are ripe and should be merged into main over the next weeks:

• ResourceScope: a wrapper around Circuit (i.e. around Hugr) that computes and caches the lifetime of "resources", i.e. linear values that are passed to and output from operations.
• Subcircuit: a new struct that defines subgraphs as intervals on ResourceScope. The advantage of this struct is that it provides the user using the Matcher API (see below) with qubit IDs (i.e. answers to the question, does gate X and gate Y apply to the same qubits). It also makes checking convexity cheap, so that we can check convexity at every step of the matching process. This provides a guarantee to the user of the matcher API that gates will be traversed "in order". See PR
• CircuitRewrite: Replaces the current CircuitRewrite (which is just a wrapper around hugr's SimpleReplacement) to a rewrite definition that uses Subcircuits for the LHS. Fully making this change requires quite a few changes to the old-badger code, as well as to portmatching (the part of tket2 dedicated to pattern matching)
• CircuitMatcher: a new Rust trait (along with a corresponding Python protocol mirroring the Rust API) that provides an API to match rewrite LHS one operation at a time. For each operation, the user can choose to match or skip an operation, thus "growing" matches, starting from a root node.
• CircuitReplacer: a new Rust trait (along with a corresponding Python protocol mirroring the Rust API) that can be implemented to provide rewrite RHSs for matches obtained from a CircuitMatcher.
• Upgrade old-badger to use CircuitMatcher and CircuitReplacer, hence becoming new-badger!

Future research directions for Seadog

The main challenges and open construction sites are:

• hashing and convexity checking: for every rewrite that we would like to apply, we need to check that i) the subgraph that is rewritten is convex (i.e. it is not possible that replacing this subgraph with another valid subgraph would introduce any cycles in our dataflow graph) and ii) the result of the rewrite is not a graph we have already considered, obtained through hashing. Executed naively, both computations are "global", in the sense that they require a computation that scales with time O(n), linear in the size of the input. However, the various convexity checks and hashes that are performed look very very similar: after a rewrite, only a small local fraction of the overall graph has been modified. There is potential to speed these tests up for the vast majority of cases.

• the expressivity of CircuitRewrite and particularly, SiblingSubgraph. The kinds of rewrites that badger/seadog can perform are dictated by the kinds of graph transformations that we can apply on our HUGRs. Currently, everything relies on SiblingSubgraphs and SimpleReplacements, which are very limited when it comes to i) control flow, ii) classical data and computations, iii) order edges. This constrains the field of applicability of the optimisers; on the other hand, once support for these cases is added, many many edge cases pop up that make rewriting very tricky, and thus must be thought through carefully.

• overall performance issues. Badger is slow because it does not (it cannot) scale to large inputs. Seadog is slow because the code is immature. I would not be surprised if some good engineering and a couple simple heuristics would get us 10x (if not more) in performance for the same results.

• making matchers, replacers and optimisers debuggable and empowering users to work on this themselves. The CircuitMatcher and CircuitReplacer represent the first time that HUGR graphs can be matched and transformed from Python land. This is very exciting for our users, but there are a LOT of things that can go wrong, so the users will need better error messages and better debugging tools. One such tool that I personally found invaluable is hit, as it allows you to graphically see where the optimiser has gone and what transformations it has considered. More stuff like that (and more accessible stuff) is required.