Using SAT to Get the World Record on LinkedIn's Queens
29 points by zenspider
29 points by zenspider
First time in years I’ve clicked on a link with “linkedin” in the title and not regretted it.
(I’m not the author, but I submitted it for them because their account is too new to post something for an unknown domain. Hopefully this’ll clear their domain for review so they can post their own content in the future)
This practice is frowned upon if not explicitly against the rules.
I see nothing in the rules prohibiting this. I invited / vouched for the author and was sitting next to him at the café when I posted this with permission. AFAICT, this is all fine, but I’m open to correction.
The broader rule is on the about page:
Self-promotion: It’s great to have authors participate in the community, but not to exploit it as a write-only tool for product announcements or driving traffic to their work. As a rule of thumb, self-promo should be less than a quarter of one’s stories and comments.
There’s grey area here, but when this situation has happened in the past (an established member posting a new domain owned by a green account), it has very often turned into the green account going full self-promo. That’s not saying it’s going to happen now, but it does mean that @rberger will prolly be under greater scrutiny.
OTOH, if @rberger doesn’t go full self-promo — mostly posting and commenting on other people’s stories — then nobody’s gonna remember this two months from now and it’s all good
That’s obviously not the spirit of the rule. Self promotion would be something like only posting stuff related to your SaaS that makes you money. If someone keeps writing cool blog articles and posts them themselves, it seems pretty clear to me that it’s not the bad kind of self promotion that this rule targets.
That is in fact the spirit of the rule!
If someone keeps writing cool blog articles and posts them themselves, it seems pretty clear to me that it’s not the bad kind of self promotion that this rule targets.
A case like this is of course much less serious than a marketer spamming us with news of their company. That being said, the goal is indeed to have authors participate in the community, one way or another.
Actually you’re a very good example of that! While you’ve authored the three stories you have submitted here, you have also continuously participated in the comments of other stories.
No, posting your own blog excessively (i.e. not in other ways being active) is very much covered by that.
It’s frowned upon in the sense that people have gotten banned or invites disabled for posting links from unseen domains on behalf of recently invited members. It is not ergonomic to go dig this out of the mod log but it has happened.
Is it? On the chat, it’s something that I always thought was allowed. If your article isn’t good, people won’t post it for you.
This is the second time I have seen someone make a solver for the LinkedIn queens game
Some time ago u spotted this on the new crates list on crates.io: https://github.com/dschafer/qsolve
The interesting difference here is that it is built up based on heuristics and not SAT, this also means that it can explain it’s solve. Now I wonder which is faster though.
Cheating (myself)
Given the amount of work it takes to understand the powerpoint and then extrapolate it to LinkedIn queens, I really don’t think this counts as cheating :P
That also, incidentally, shows why it’s so rare for people solve problems with SAT: it’s so much effort to manually convert high-level constraints into SAT clauses, and lots of tools can already do it for you! For example, some of this could be simplified with z3’s forall.
I appreciate the encouragement. Sometimes peeking at the answer can feel like cheating (although I now feel much more confident that I could solve other SAT problems without “peeking” such as graph coloring)
I’m very curious about using forall though. Maybe you could hint me in the right direction? Are you thinking about modeling this as a tuple via declare-fun and then forall’ing some properties inside them?
Okay so I thought one example would be replacing at_most_one with something along the lines of
n = len(elems)
x, y = Ints('x y')
at_most_one_list = ForAll([x, y], Implies(x != y, Or(Not(elems[x]), Not(elems[y])))
But it turns out that z3 at least can’t index a Python list off a z3 variable. I think in this case you’re supposed to lift the all to a Python loop, but you’ve already got that, so it’s not very helpful. After spending an hour reading the Z3 API, though, I found out about AtLeast and AtMost. So we can write
def exactly_one(elems: List[Bool]):
return And(
AtLeast(*elems, 1),
AtMost(*elems, 1)
)
Again, this is specifically for Z3, I don’t know if CVC5 has the same functionality.
Ah! That would be much more ergonomic if it were possible.
I would be surprised if CVC5 had similar convenience methods (couldn’t find any in the docs). The Pythonic bindings were lacking compared to Z3’s. I did the initial N-Queens in Z3 and then adapted it to CVC5 (for learning purposes) and there were quite a few more edge cases (i.e. what happens when you pass a list with a single element in an And? CVC5 will crash, Z3 understands that it is a no-op, and returns just the argument).
I should probably see if CVC5 wants those sorts of contributions because it wouldn’t be too hard to add…
Okay so I felt a little bad about sending you down a goose chase, so I goose chased myself and figured out a higher level SMT representation of the problem that should work for CVC5 too. The idea is that instead of using N² booleans to represent the queen’s positions, we instead use N integers: queens[0] is the column of the queen on row 0, queens[1] the queen on row 1, etc. This automatically gives us ExactlyOne queen per row, and then ExactlyOne per column is just i != j for i, j in combinations(q, 2). Finally, we can simplify NoAdjacency by noting that every possibly remaining adjacency must be of the form abs(queens[row] - queens[row-1]) == 1. After that it’s just a (very tedious and error prone) matter of coding in the regions.
I put a z3 example up here: https://gist.github.com/hwayne/c5de7bc52e733995311236666bedecd3 . It’s super messy and I didn’t clean up any of the testing code I wrote, but gets the idea across. I did a skim and it seems all of the same APIs are present in CVC5 too, though you’d have to handle the edge case of size-1 regions.
interesting, that sort of Exactly-One-Per-Row,Column,Diagonal transform is also how N-Queens was optimized for Clingo / Dusa
https://arxiv.org/pdf/2405.19040 page 44
It’s beside the point of the article, but it’s a bit confusing that LinkedIn calls the game “queens” if two nonadjacent pieces are allowed to occupy the same diagonal. If the idea is that no piece threatens any other, then these pieces seem to behave like shogi’s dragon kings
I agree ;), outside of Microsoft they use stars. I hadn’t heard of that piece before, that’s really neat.
I’ve been playing around with logic langs like Potassco recently trying to solve puzzles like this, so it’s really nice seeing the process.
Just for broader context - the LinkedIn Queens puzzle is more commonly known as ‘Star Battle’ https://www.puzzles.wiki/wiki/Star_Battle
Where’s the code?
I’ve pushed it up here: https://github.com/ryan-berger/queens/blob/master/main.py
I’ll link it to in article as an edit in just a second
That’s incredible timing: my bachelor thesis is about solving another LinkedIn game (Tango) using SAT and Pseudo-Boolean solvers. I haven’t looked at Queens closely enough, but I think that a Pseudo-Boolean model might be easier to formulate and reason about, since you can directly encode = and > constraints directly.