Yeah, it's only been like a month since I released version v0.1. I also didn't really say anything about that release, even though it's the very first official release of Saturn V. Well, that's because it isn't really a big deal! Just release early, release often.

No, I don't have testers or users yet, but whatever. I'm still ironing out the release pipeline, since (fun fact) this is the very first time I've ran a hobby project that had "real" binary releases and I wasn't just eternally trapped in pre-alpha. Well, that changes now... even if it means that I have to spend consecutive late nights figuring out how the hell to get GitHub Actions to compile Saturn V release builds on OpenBSD (more on that later).

WebAssembly bindings

One of the coolest parts about Saturn V is that because it's written in Rust, it can support compiling to a variety of non-native architectures. Support for WebAssembly means that Saturn V can run in a web browser, which opens up a whole host of embedding and interop possibilities.

Pure WebAssembly VSCode extension

One use of WebAssembly is that the VSCode extension now embeds a WebAssembly build of the Kerolox language server instead of using the system's native Saturn V installation. This means that once the extension is on the Marketplace, getting started with Kerolox development is a one-click installation!

Client in Wasm

The Saturn V web client library also runs in Wasm now. I've exposed bindings to it for Javascript/Typescript projects to use directly. I'm not using them myself yet, but it was pretty trivial to add bindings thanks to wasm-bindgen. This provides people who might want to develop JS-based frontends for Saturn V a framework to use.

Rudimentary Python bindings

On the topic of bindings, I also spent a fair bit of time trying to build Python bindings to the client API. Most of the boilerplate is in place such as a testing framework and automatic CI checking, but I struggle to take it the rest of the way on my own due to my lack of personal familiarity with Python idioms.

I'm tracking the development of the rest of the Python API in a GitHub milestone. If you see anything that you could help out with, please consider contributing!

Orbital sim

Behold! The most overengineered loading icon of all time.

It all started when I was in my calculus II class during the summer of 2025. A classmate brought up the three-body problem in passing, so of course I look it up on Wikipedia for reference. Scrolling through it, I noticed this really fantastic visualization of a variety of specific periodic solutions:

By Perosello - Uploaded by Author, CC BY-SA 4.0, Link

My first thought was, "Hey, wouldn't that make for an awesome loading icon?"

I then decided to display three-body solutions throughout the various interfaces I make for Saturn V as an indicator for when Saturn V is processing the latest data and forming its decisions.

The three-body problem is a challenge within Newtonian physics of predicting where three bodies (like planets, moons, stars, wherever) are going to move, assuming that they exert a gravitational pull on each other and follow Newton's laws of motion. A periodic solution to the three-body problem is finding ways to arrange three bodies such that they orbit themselves in a stable loop. With two bodies, finding stable orbits is relatively straight-forward (thank you, Kepler). However, because of chaos theory, three bodies are much harder to mathematically find periodic solutions to. They are also exceedingly rare in nature because of the very special circumstances required to keep three bodies in a stable orbit around each other.

Despite the complex physics topics involved in the study of the three-body problem, it's quite easy to intuitively grasp that periodic solutions to the three-body solution are remarkable just by looking at them.They simply look unnatural, but they completely follow the usual physical laws we take for granted. Their beauty exists on the fringe between order and chaos.

To me, this is a really effective metaphor for Saturn V. Saturn V works under completely logical and natural mechanisms, but because it is crafted purposefully, it's able to create these complex, special structures that are otherwise impossible for humans to regulate manually. I can think of other examples of this sort of "controlled chaos" that would also express Saturn V's relationship with the natural world, but the three-body problem is unique because of its visual intuition and shared space theme.

How the orbital sim works

This is a sidetrack into how I implemented the orbital sim, so feel free to skip this section, especially if you're not very interested in the mathematics of orbital mechanics.

The bottom line of it is that I begin with the positions, velocities, and masses of three bodies from a known solution to the three-body problem. I simulate those bodies using traditional Newtonian mechanics for as long as the solution specifies the period lasts. I also take advantage of the time-reversibility of Newtonian mechanics to simulate the bodies in reverse for the same period, and linearly interpolate the two simulations end-to-end to correct for any drifting between the positions of the bodies at the endpoints of the sim caused by the lack of floating-point precision.¹

Once all the position data for the entirety of the simulation is calculated, the real trick is to then take the discrete Fourier transform of the positions of the bodies. Because all periodic three-body solutions are highly elliptical, a handful of the frequency components per-body contain the vast majority of the information about the orbit. I discard all frequency components above a certain amplitude, retaining only that small number of dominant components. This is what's saved to disk. This concludes the "baking" phase of the orbital sim, which is ran as part of Saturn V's build process.

At runtime, I can load the baked frequency domains for each body for each orbit. Then, using a couple standard trigonometric functions, I can reconstruct the position of each body at arbitrary timesteps with a very high degree of accuracy to the original simulation data. I use this to rapidly compute the points to render the path trail on, as well as to determine the position of each body during subframes for the motion blur. By default, the renderer draws 10 motion blur subframes and 20 path segments for each of the 3 bodies, so that requires in 10 * 20 * 3 = 600 orbit lookups per frame. I haven't profiled it, but the renderer runs in WebAssembly and renders the result to a browser canvas with zero lag or stutter, even on mobile browsers. "Great success," as a certain fictional Kazakh journalist would say.

MaxSAT solver goes vroom vroom

You may have heard me babble about SAT (aka the Boolean satisfiability problem). SAT solvers are how Saturn V makes its decisions. MaxSAT (particularly partial weighted MaxSAT) is how Saturn V determines that some decisions are better than others.

For example, let's take this Saturn V program:

; Each possible coordinate on the board.
define output Coord Integer.
Coord 1.
Coord a :- Coord b, b < 8, a = b + 1.

; Each possible placement of a queen.
define output decision Queen(Coord, Coord).
Queen(row, col) :- Coord row, Coord col.

; At most one queen goes on each row.
constrain(row) <= 1 :- Queen(row, col).

; At most one queen goes on each column.
constrain(col) <= 1 :- Queen(row, col).

; At most one queen can go along each main diagonal.
constrain(diag) <= 1 :- Queen(row, col), diag = row + col.

; At most one queen can go along each orthogonal diagonal.
constrain(diag) <= 1 :- Queen(row, col), diag = row - col.

; Try to place as many queens as possible.
constrain soft(1) (coord) = 1 :- Queen coord.

This is identical to the n-queens example except that instead of specifying that exactly one queen goes on each row and column, at most one queen goes on each row and column. Because this allows Saturn V to place no queens on the board, we also add that last soft constraint:

; Try to place as many queens as possible.
constrain soft(1) (coord) = 1 :- Queen coord.

Whereas n-queens is a basic constraint solving problem, this variation of it is an optimization problem. We're trying to place, using a soft constraint, one queen on every coordinate. The difference between soft constraints and regular constraints is that Saturn V can choose to ignore soft constraints... but there's a cost penalty. The cost of this constraint is 1 per queen that isn't placed on a coordinate.

When Saturn V runs this program, it attempts to find a solution that minimizes its cost. Our knowledge of the n-queens problem tells us that for any board of size n on a side can fit up to n queens on it. However, Saturn V has to figure this out itself. This is the optimization aspect of the program.

Prior to version 0.2, Saturn used ran what's called in the literature a linear UNSAT-SAT search to attempt to find the optimum solution. This uses a SAT solver to find the minimum number of soft constraints that can be violated (i.e. the maximum number of queens) while meeting all hard constraints. It first queries if an ideal solution is satisfiable. If that query is UNSAT, then it queries if there is a satisfying solution with a cost of 1. It repeats until it finds a SAT solution, which becomes the lowest-possible cost of any SAT solution.

To anthropomorphize a bit, this is Saturn V's pre-v0.2 approach:

Can all queens fit on the board?
  ...no.
Can all but 1 queen fit on the board?
  ...no.
Can all but 2 queens fit on the board?
  ...no.
Can all but 3 queens fit on the board?
  ...no.
Can all but 4 queens fit on the board?
  ...
  <et cetera>
  ...
Can all but 55 queens fit on the board?
  ...no.
Can all but 56 queens fit on the board?
  ...yes!

Saturn V has found the optimal solution: all but 56 positions can fit a queen on an 8x8 chess board. When Saturn V next reads the output of the SAT solver, it will find that the SAT solver has placed 8 queens on the chess board.

However, that's really, really slow! What if we want to see how many queens can fit on a 100x100 chessboard? We have to first ask if all 10,000 queens fit, then if 9,999 queens fit, then if 9,998 queens fit, et cetera, until we converge on the correct answer, which is that 100 queens can fit. More importantly, it's generally much more difficult for SAT solvers to prove that a complex constraint problem like this is UNSAT than it is to find a solution a SAT problem. This means that for every number of queens that is UNSAT, the SAT solver has to do a lot of work just to move on to one fewer queen and start all over.

For version v0.2, I've switched Saturn V to instead use a linear SAT-UNSAT search for the optimal solution.

Saturn V now thinks for an 8x8 chess board:

Can 0 queens fit on the board?
  ...yes.
Can 1 queen fit on the board?
  ...yes.
Can 2 queens fit on the board?
  ...yes.
Can 3 queens fit on the board?
  ...yes.
Can 4 queens fit on the board?
  ...yes.
Can 5 queens fit on the board?
  ...yes.
Can 6 queens fit on the board?
  ...yes.
Can 7 queens fit on the board?
  ...yes.
Can 8 queens fit on the board?
  ...yes.
Can 9 queens fit on the board?
  ...no!

Saturn V can conclude that whichever solution the SAT solver has found for 8 queens is the best solution, and that's what it uses as the result. This only takes 10 queries to the SAT solver instead of 57 queries. For a 100x100 board, it would now make at most 102 queries instead of at most 9,901 queries².

Additionally, the SAT solver is doing significantly less work per query. In linear SAT-UNSAT, you can imagine that the SAT solver is gradually placing more queens on the board over time. If it can place more queens while reusing valid placements, it doesn't need to recalculate why those queens are there in the first place. If adding new queens gets in the way of existing queens, it can shuffle them around to make room. This is much easier for the SAT solver than needing to prove from scratch for each count of queens why that number of queens doesn't fit.

Non-monotonic reasoning

I've implemented support for non-monotonic reasoning. "Non-monotonic reasoning" is just fancy math lingo for saying that Saturn V can now make decisions based on rules not being applicable. You can see this being used in the Laundry.rp1 example to reason about what clothes are available to wear in a day:

; Carry over wardrobe items from yesterday if they were not worn.
Wardrobe(today, article) :-
    Wardrobe(yesterday, article),
    !Outfit(yesterday, article),
    Day(today),
    today = yesterday + 1.

That "not" symbol, !, is the non-monotonic part. In plain language, this rule means that the clothes available in a wardrobe are whichever clothes were both in the wardrobe yesterday and weren't part of an outfit yesterday. This sort of reasoning was a bit of a pain to get working but is crucial for intuitively expressing common situations like "wearing an article of clothing today means it's not available to wear tomorrow."

How non-monotonic reasoning works

The technical side of non-monotonic reasoning is very complicated. The best sources for what I'm talking about are computer science research papers. Again, feel free to skip this section if you're not interested in the nitty-gritty of logic programming.

I assign a stratum (natural number) to each relation in a program using a topological sort of each relation's non-monotonic dependencies on other relations. Then, I defer evaluation of the refutation nodes in the dataflow representation of the program until all strata beneath that node's stratum have been evaluated. This is bog-standard stratified negation³.

However, within each dataflow stratum, I also technically evaluate local stratification⁴ using dual fixed-points (positive semi-naive inference and negation-as-failure). This means relations can have mutually non-monotonic effects on one another.⁵ However, I'm committed to supporting at most one stable model per program evaluation so as to not make Saturn V a general answer set programming implementation. To support local stratification without permitting more than one stable model, I'm going to use the "check" step of Kerolox compilation to verify the completeness of the well-founded semantics of Kerolox programs.⁶ I haven't done that yet (since the "check" step isn't even part of the pipeline right now), but the infrastructure is in place. For now, you can only write Kerolox programs with globally-stratified negation semantics.

OpenBSD

Right, so, OpenBSD. My lovely partner Emma maintains a local OpenBSD-based homelab, so I figured it would be a fun (and useful!) challenge to get my Saturn V server to run on that. Well, now CI automatically compiles binary release builds for OpenBSD! I don't know if they run but they certainly compile. That's pretty awesome.

Someday soon, I'd like to set up an OpenBSD-based computer at home to run a personal Saturn V instance 24/7. I chose OpenBSD to run my personal instance because it is exceedingly lightweight and has all the tooling to do HTTPS relaying and automatic TLS certificate generation built-in.

I'll write about how that goes in follow-up posts!

Where to next?

My main priority now is to develop a practical application using Saturn V. Many of the changes in this release were a result of me experimenting with using the engine in full applications. In the time before the next release, I'm going to focus strongly on making full application development a reality. I've put about a year of work into Saturn V, it's about damn time I start getting some use out of it!

Right now, I use server-sent event (SSE) subscriptions in order to receive live updates to the results of the Saturn V solver. However, I've found out in my experimentation that web browsers only allow a page to keep a handful of SSE subscriptions open, since it's not really meant to be used for data-heavy systems like Saturn V. I'd like to put in the time to develop a proper RPC API to the server over WebSocket. This is something I've wanted to do for a long time and will let clients do some really neat stuff like atomic transactions on inputs.

Next, I'm going to spend some time integrating the Saturn V client into Leptos idiomatically. This shouldn't be difficult once the RPC system is fleshed out.

Finally, I'm going to use Leptos to make a full, practical app using Saturn V. I've decided to make a meal planner, since deciding what to eat every day is something I chronically struggle with in particular. Fingers crossed that it works out!

Until next time. See you, space cowboy.