No newsletter next week I’ll be speaking at Systems Distributed. My talk isn't close to done yet, which is why this newsletter is both late and short. Solving LinkedIn Queens in SMT The article Modern SAT solvers: fast, neat and underused claims that SAT solvers1 are "criminally underused by the industry". A while back on the newsletter I asked "why": how come they're so powerful and yet nobody uses them? Many experts responded saying the reason is that encoding SAT kinda sucked and they rather prefer using tools that compile to SAT. I was reminded of this when I read Ryan Berger's post on solving “LinkedIn Queens” as a SAT problem. A quick overview of Queens. You’re presented with an NxN grid divided into N regions, and have to place N queens so that there is exactly one queen in each row, column, and region. While queens can be on the same diagonal, they cannot be adjacently diagonal. (Important note: Linkedin “Queens” is a variation on the puzzle game Star Battle, which is the same except the number of stars you place in each row/column/region varies per puzzle, and is usually two. This is also why 'queens' don’t capture like chess queens.) Ryan solved this by writing Queens as a SAT problem, expressing properties like "there is exactly one queen in row 3" as a large number of boolean clauses. Go read his post, it's pretty cool. What leapt out to me was that he used CVC5, an SMT solver.2 SMT solvers are "higher-level" than SAT, capable of handling more data types than just boolean variables. It's a lot easier to solve the problem at the SMT level than at the SAT level. To show this, I whipped up a short demo of solving the same problem in Z3 (via the Python API). Full code here, which you can compare to Ryan's SAT solution here. I didn't do a whole lot of cleanup on it (again, time crunch!), but short explanation below. The code from z3 import * # type: ignore from itertools import combinations, chain, product solver = Solver() size = 9 # N Initial setup and modules. size is the number of rows/columns/regions in the board, which I'll call N below. # queens[n] = col of queen on row n # by construction, not on same row queens = IntVector('q', size) SAT represents the queen positions via N² booleans: q_00 means that a Queen is on row 0 and column 0, !q_05 means a queen isn't on row 0 col 5, etc. In SMT we can instead encode it as N integers: q_0 = 5 means that the queen on row 0 is positioned at column 5. This immediately enforces one class of constraints for us: we don't need any constraints saying "exactly one queen per row", because that's embedded in the definition of queens! (Incidentally, using 0-based indexing for the board was a mistake on my part, it makes correctly encoding the regions later really painful.) To actually make the variables [q_0, q_1, …], we use the Z3 affordance IntVector(str, n) for making n variables at once. solver.add([And(0 <= i, i < size) for i in queens]) # not on same column solver.add(Distinct(queens)) First we constrain all the integers to [0, N), then use the incredibly handy Distinct constraint to force all the integers to have different values. This guarantees at most one queen per column, which by the pigeonhole principle means there is exactly one queen per column. # not diagonally adjacent for i in range(size-1): q1, q2 = queens[i], queens[i+1] solver.add(Abs(q1 - q2) != 1) One of the rules is that queens can't be adjacent. We already know that they can't be horizontally or vertically adjacent via other constraints, which leaves the diagonals. We only need to add constraints that, for each queen, there is no queen in the lower-left or lower-right corner, aka q_3 != q_2 ± 1. We don't need to check the top corners because if q_1 is in the upper-left corner of q_2, then q_2 is in the lower-right corner of q_1! That covers everything except the "one queen per region" constraint. But the regions are the tricky part, which we should expect because we vary the difficulty of queens games by varying the regions. regions = { "purple": [(0, 0), (0, 1), (0, 2), (0, 3), (0, 4), (0, 5), (0, 6), (0, 7), (0, 8), (1, 0), (2, 0), (3, 0), (4, 0), (5, 0), (6, 0), (7, 0), (8, 0), (1, 1), (8, 1)], "red": [(1, 2), (2, 2), (2, 1), (3, 1), (4, 1), (5, 1), (6, 1), (6, 2), (7, 1), (7, 2), (8, 2), (8, 3),], # you get the picture } # Some checking code left out, see below The region has to be manually coded in, which is a huge pain. (In the link, some validation code follows. Since it breaks up explaining the model I put it in the next section.) for r in regions.values(): solver.add(Or( *[queens[row] == col for (row, col) in r] )) Finally we have the region constraint. The easiest way I found to say "there is exactly one queen in each region" is to say "there is a queen in region 1 and a queen in region 2 and a queen in region 3" etc." Then to say "there is a queen in region purple" I wrote "q_0 = 0 OR q_0 = 1 OR … OR q_1 = 0 etc." Why iterate over every position in the region instead of doing something like (0, q[0]) in r? I tried that but it's not an expression that Z3 supports. if solver.check() == sat: m = solver.model() print([(l, m[l]) for l in queens]) Finally, we solve and print the positions. Running this gives me: [(q__0, 0), (q__1, 5), (q__2, 8), (q__3, 2), (q__4, 7), (q__5, 4), (q__6, 1), (q__7, 3), (q__8, 6)] Which is the correct solution to the queens puzzle. I didn't benchmark the solution times, but I imagine it's considerably slower than a raw SAT solver. Glucose is really, really fast. But even so, solving the problem with SMT was a lot easier than solving it with SAT. That satisfies me as an explanation for why people prefer it to SAT. Sanity checks One bit I glossed over earlier was the sanity checking code. I knew for sure that I was going to make a mistake encoding the region, and the solver wasn't going to provide useful information abut what I did wrong. In cases like these, I like adding small tests and checks to catch mistakes early, because the solver certainly isn't going to catch them! all_squares = set(product(range(size), repeat=2)) def test_i_set_up_problem_right(): assert all_squares == set(chain.from_iterable(regions.values())) for r1, r2 in combinations(regions.values(), 2): assert not set(r1) & set(r2), set(r1) & set(r2) The first check was a quick test that I didn't leave any squares out, or accidentally put the same square in both regions. Converting the values into sets makes both checks a lot easier. Honestly I don't know why I didn't just use sets from the start, sets are great. def render_regions(): colormap = ["purple", "red", "brown", "white", "green", "yellow", "orange", "blue", "pink"] board = [[0 for _ in range(size)] for _ in range(size)] for (row, col) in all_squares: for color, region in regions.items(): if (row, col) in region: board[row][col] = colormap.index(color)+1 for row in board: print("".join(map(str, row))) render_regions() The second check is something that prints out the regions. It produces something like this: 111111111 112333999 122439999 124437799 124666779 124467799 122467899 122555889 112258899 I can compare this to the picture of the board to make sure I got it right. I guess a more advanced solution would be to print emoji squares like 🟥 instead. Neither check is quality code but it's throwaway and it gets the job done so eh. "Boolean SATisfiability Solver", aka a solver that can find assignments that make complex boolean expressions true. I write a bit more about them here. ↩ "Satisfiability Modulo Theories" ↩

Go 1.23 adds iterators. An iterator is a way to provide values that can be used in for x := range iter loops. People are happy the iterators were added to the language. Not everyone is happy about HOW they were implemented. This person opined that they demonstrate “typical Go fashion of quite ugly syntax”. The ugly Are Go iterators ugly? Here’s the boilerplate of an iterator: func IterNumbers(n int) func(func(int) bool) { return func(yield func(int) bool) { // ... the code } } Ok, that is kind of ugly. I can’t imagine typing it from memory. The competition We do not live in a vacuum. How do other languages implement iterators? C++ I recently implemented DirIter class with an iterator in C++, for SumatraPDF. I did it to so that I can write code like for (DirEntry* e : DirIter("c:\")) { ... } to read list of files in directory c:\. Implementing it was no fun. I had to implement a class with the following methods: begin() end() DirEntry* operator*() operator==() operator!=() operator++() operator++(int) Oh my, that’s a lot of methods to implement. A bigger problem is that the logic is complicated. This is an example of pull iterator where the caller “pulls” next value out of the iterator. The caller needs at least two operations from an iterator: give me next value do you have more values? In C++ it’s more complicated than that because “Overcomplication” is C++’s middle name. A function that reads a list of entries in a directory is relatively simple. The difficulty of implementing pull iterator comes from the need to track the current state of iteration to be able to provide “give me next value” function. A simple directory traversal turned into complicated tracking of what I have read so far, did the process finish and reading the next directory entry. C C# also has pull iterators but they removed incidental complexity present in C++. It reduced the interface to just 2 essential methods: T Next() which returns next element bool HasMore() which tells if there are more values to read Here’s an iterator that returns integers from 1 to n: class NumberIterator { private int _current; private int _end; public NumberIterator(int n) { _current = 0; _end = n; } public bool HasMore() { return _current < _end; } public int Next() { if (!HasMore()) { throw new InvalidOperationException("No more elements."); } return ++_current; } } Much better but still doesn’t solve the big problem: the logic is split across many calls to Next()so the code needs to track the state. C# push iterator with yield Later C# improved this by adding a way to implement push iterator. An iterator is just a function that “pushes” values to the caller using a yield statement. Push iterator is much simpler: static IEnumerable<int> GetNumbers(int n) { for (int i = 1; i <= n; i++) { yield return i; } } Clever and elegant Here’s a Go version: func GetNumbers(n int) func(func(int) bool) { return func(yield func(int) bool) { for i := i; i <= n; i++ { if !yield(i) { return } } } } The clever and elegant part is that Go designers figured out how to implement push iterators in a way very similar to C#’s yield without adding new keyword. The hard part, the logic of the iterator, is equally simple as with yield. The yield statement in C# is kind of magic. What actually happens is that the compiler rewrites the code inside-out and turns linear logic into a state machine. Go designers figured out how to implement it using just a function. It is true that there remains essential complexity: iterator is a function that returns a function that takes a function as an argument. That is a mind bend, but it can be analyzed. Instead of yield statement pushing values to the loop driver, we have a function. This function is synthesized by the compiler and provided to the iterator function. The argument to that function is the value we’re pushing to the loop. It returns a bool to indicate early exit. This is needed to implement early break out of for loop. An iterator function returns an iterator object. In Go case, the iterator object is a new function. This creates a closure. If function is an iterator object then local variables of the function are state of the iterator. I don’t know why Go designers chose this design over yield. I assume the implementation is simpler so maybe that was the reason. Or maybe they didn’t want to add new keyword and potentially break existing code.

Dan Abramov in “Static as a Server”: Static is a server that runs ahead of time. “Static” and “dynamic” don’t have to be binaries that describe an entire application architecture. As Dan describes in his post, “static” or “dynamic” it’s all just computers doing stuff. Computer A requests something (an HTML document, a PDF, some JSON, who knows) from computer B. That request happens via a URL and the response can be computed “ahead of time” or “at request time”. In this paradigm: “Static” is server responding ahead of time to an anticipated requests with identical responses. “Dynamic” is a server responding at request time to anticipated requests with varying responses. But these definitions aren’t binaries, but rather represent two ends of a spectrum. Ultimately, however you define “static” or “dynamic”, what you’re dealing with is a response generated by a server — i.e. a computer — so the question is really a matter of when you want to respond and with what. Answering the question of when previously had a really big impact on what kind of architecture you inherited. But I think we’re realizing we need more nimble architectures that can flex and grow in response to changing when a request/response cycle happens and what you respond with. Perhaps a poor analogy, but imagine you’re preparing holiday cards for your friends and family: “Static” is the same card sent to everyone “Dynamic” is a hand-written card to each individual But between these two are infinite possibilities, such as: A hand-written card that’s photocopied and sent to everyone A printed template with the same hand-written note to everyone A printed template with a different hand-written note for just some people etc. Are those examples “static” or “dynamic”? [Cue endless debate]. The beauty is that in proving the space between binaries — between what “static” means and what “dynamic” means — I think we develop a firmer grasp of what we mean by those words as well as what we’re trying to accomplish with our code. I love tools that help you think of the request/response cycle across your entire application as an endlessly-changing set of computations that happen either “ahead of time”, “just in time”, or somewhere in-between. Email · Mastodon · Bluesky

I recently wrote about How to Use SSH with FIDO2/U2F Security Keys, which I now use on almost all of my machines. The last one that needed this was my Raspberry Pi hooked up to my DEC vt510 terminal and IBM mechanical keyboard. Yes I do still use that setup! To my surprise, generating a … Continue reading I Learned We All Have Linux Seats, and I’m Not Entirely Pleased →

Back in 2017–2020, while I was on the Blaze team at Google, I took on a 20% project that turned into a bit of an obsession: sandboxfs. Born out of my work supporting iOS development, it was my attempt to solve a persistent pain point that frustrated both internal teams and external users alike: Bazel’s