As a professional haskeller, I feel it necessary to point out for people in this thread who are less exposed to Haskell and who may be Haskell-curious...this is not what real-world commercial Haskell code looks like. To use a C analogy, I'd say it's closer to IOCCC entries than Linux kernel code.
Thanks for that. Having read the article, I was left with the overwhelming impression that I'd have solved it in a totally different way if I was trying in OCaml.
Briefly, I'd have started with an array which for each colour had an array containing the coordinate pairs for that colour. I'd probably then have sorted by length of each array. The state also has an empty array for the coordinates of each placed queen.
To solve, I'd take the head array as my candidates, and the remaining array of arrays as the next search space. For each candidate, I'd remove that coordinate and anything that was a queen move from it from the remaining arrays, and recursively solve that. If filtering out a candidate coordinate results in an empty list for any of the remaining arrays, you know that you've generated an invalid solution and can backtrack.
At no point would I actually have a representation of the board. That feels very imperative rather than functional to me.
To me, this solution immediately jumps out from the example - one of the queens in on a colour with only 1 square, so it HAS to be there. Placing that there immediately rules out one of the choices in both colours with 2 squares, so their positions are known immediately. From that point, the other 2 large regions have also been reduced to a single candidate each.
Yeah, comparing to how you'd solve this in any other mainstream language is really an apples-to-oranges comparison here because this is explicitly tackling the contrived problem of solving it at the type level rather than at the much more common value level. Very few languages in existence have the ability to do this kind of type-level computation. I'd say Haskell is really the only language that could conceivably be called "viable for mainstream use" that currently supports it, and even in Haskell's case the support is new, largely experimental, in a state of active research, and not well integrated with the ergonomics of the rest of the language.
As someone who has never touched Haskell and who knows nearly nothing about it, Haskell is not, in fact, a "dynamically typed, interpreted language", which, "has no currying".
At the risk of explaining away a perfectly good joke, that person is writing programs at the type level. The joke is that the type system is turing complete if you enable the right extensions.
This gives me a message "Unavailable Due to the UK Online Safety Act" which sounds like nonsense for a blog post, but IANAL. Can anyone summarise the post, or suggest why there'd be a reason my online safety is compromised by it?
It's pretty clear that the issue is not the post, but the fact that you are in UK, and the site author does not deem you important enough.
The site author himself has blocked users from the UK because of that stupid law that you cite in your comment:
"The UK's Online Safety Act requires operators of 'user to user services' to read through hundreds (if not thousands) of pages of documentation to attempt to craft "meaningful" risk assessments and 'child access assessments' or face £18,000,000 fines, even imprisonment."
I set this as part of a Scala programming assignment for my second year undergraduate class at UNE (Australia) last term. However, during the working a square is not Queen | Eliminated but Set[Queen | NotQueen]
Largely so from a programming perspective it becomes a simplified version of Einstein's Riddle that I showed the class, doing in a similar way.
thanks for saying this, that is how I play this game usually, and I was confused by TFA going with backtracking/guessing a next attempt, when constraint propagation seems easier, I thought I was missing something.
Just when I start thinking I am smart, someone drops this :) Haskell certainly looks graceful but is imposing! I feel pretty good if I can do functional stuff in Rust, but this is next level.
I think it's helpful to separate out the "Haskell is imposing" from "This language that I don't know is imposing". It is unrealistic to expect to be able to read a language you don't know. It is easy to be accidentally trained otherwise, because there are several languages out there that are hardly different from each other except in unimportant details and in a perfect world perhaps we wouldn't need both of them, and if you work with a couple of them you might get used to being able to read across languages, but those are really the exceptions rather than the rule. Even if they are very, very large and popular exceptions.
I won't say this reduces the "Haskell is imposing" to zero, but a non-trivial amount of the initial impression of imposingness is just the very different syntax, such as the way functions are not called with parentheses after the function name. But the different syntax isn't really that big a deal. You just don't know it and aren't used to it. Under the hood it does have some differences, but the differences are magnified when you try to swallow the surface differences and the deep differences all in one shot. Nobody who knows Haskell did that; they learned it the same way you learn any other language, one bit at a time.
I believe I first encountered this problem while working through SICP. Was confused why it's called Linkedin queens, since this problem is a classical one in CS that definitely pre-dated the existence of Linkedin.
LinkedIn's daily Queens puzzle is different than the classical problem in two ways: it adds colored regions which also must have exactly one queen, and it relaxes the diagonal constraint -- queens are allowed in the same diagonal as long as they are not adjacent.
1) It's not too hard to make a problem with at least one solution (just put the queens down first, then draw boxes), but there isn't any good way of making levels with unique solutions.
2) Once you've accomplished that, it's hard to predict how hard a level will be, and then it's hard to make levels easier / harder.
I happen to be currently researching this topic (well, I'm doing all kinds of these grid-based puzzles, but this is an example). The algorithm tries to make "good" levels, but there is a good probability it will end up with something useless we need to throw away, and then try again.
It's easy to make levels which are trivial, and similarly easy to make levels which are far beyond human ability, but hitting things in the 'human tricky but solvable' sweet-spot is where most of the difficulty comes from.
I should probably try writing up a human-readable version of how I do it. It involves a bunch of Rust code, so I can hit a whole bunch of trendy topics!
> I should probably try writing up a human-readable version of how I do it. It involves a bunch of Rust code, so I can hit a whole bunch of trendy topics!
Given that this could be a variant of "exact cover", using zdds to explore the problem space might simplify finding exact puzzles in addition to puzzles that require lookahead.
Generally what is needed is a subroutine that can tell you 1) if the problem has a solution, and 2) if the solution is unique (common requirement for puzzles like these). Using such a model as a sub-routine, a heuristic search can be done to gradually build up puzzles. If your solver technology of choice can handle quantified problems, that could be used to integrate those two problems into one, but that is quite a lot harder to to.
If the base solver you have is a system that can be run in various configurations with different levels of reasoning and assumption as well as a report on the amount of search needed if any, that can be very useful as a way to measure the hardness. In Sudoku as a Constraint problem (https://citeseerx.ist.psu.edu/document?doi=4f069d85116ab6b4c...), Helmut Simonis tested lots of 9x9 Sudoku puzzles against various levels of propagation and pre-processing as a way to measure the hardness of Sudoku puzzles by categorizing them by the level of reasoning needed to solve without search. The MiniZinc model for LinkedIn Queens (https://news.ycombinator.com/item?id=44353731) can be used with various solvers and levels of propagation as such a subroutine.
Now, for production-level puzzle making, such as what King does for Candy Crush, the problems and requirements are even harder. I've heard presentation where they talk about training neural networks to play like human testers, so not optimal play but most human like play, in order to test the hardness level of the puzzles.
It's the same problem as with generating good sudoku boards. It's not easy, and there's not many publicly available solutions, but solutions exist.
A common opinion is that a good board is solvable without the use of backtracking. A set of known techniques should be enough to solve the board. To validate if a board is "fun" you need to have a program that can solve the board using these known techniques. Making that program is much harder than just making a general solver. And then you need to find the boards that can be validated as fun. Either you search through random boards, or you get clever...
I've noticed that puzzles that can be solved with CP-SAT's presolver so that the SAT search does not even need to be invoked basically adhere to this (no backtracking, known rules), e.g.:
#Variables: 121 (91 primary variables)
- 121 Booleans in [0,1]
#kLinear1: 200 (#enforced: 200)
#kLinear2: 1
#kLinear3: 2
#kLinearN: 30 (#terms: 355)
Presolve summary:
- 1 affine relations were detected.
- rule 'affine: new relation' was applied 1 time.
- rule 'at_most_one: empty or all false' was applied 148 times.
- rule 'at_most_one: removed literals' was applied 148 times.
- rule 'at_most_one: satisfied' was applied 36 times.
- rule 'deductions: 200 stored' was applied 1 time.
- rule 'exactly_one: removed literals' was applied 2 times.
- rule 'exactly_one: satisfied' was applied 31 times.
- rule 'linear: empty' was applied 1 time.
- rule 'linear: fixed or dup variables' was applied 12 times.
- rule 'linear: positive equal one' was applied 31 times.
- rule 'linear: reduced variable domains' was applied 1 time.
- rule 'linear: remapped using affine relations' was applied 4 times.
- rule 'presolve: 120 unused variables removed.' was applied 1 time.
- rule 'presolve: iteration' was applied 2 times.
Presolved satisfaction model '': (model_fingerprint: 0xa5b85c5e198ed849)
#Variables: 0 (0 primary variables)
The solution hint is complete and is feasible.
#1 0.00s main
a a a a a a a a a a *A*
a a a b b b b *B* a a a
a a *C* b d d d b b a a
a c c d d *E* d d b b a
a c d *D* d e d d d b a
a f d d d e e e d *G* a
a *F* d d d d d d d g a
a f f d d d d d *H* g a
*I* i f f d d d h h a a
i i i f *J* j j j a a a
i i i i i k *K* j a a a
Together with validating that there is only 1 solution you would probably be able to make the search for good boards a more guided than random creation.
Simulated annealing with a difficulty heuristic (like minimum required logical steps) works well - start with a valid solution, then randomly modify colors while maintaining uniqueness.
Awesome, I'm writing a "logical solver" just like this - I'll hopefully also have something to post here when I'm done.
I'm trying to use it during the generation process to evaluate the difficulty a basic heuristic I'm trying to work with is counting the number of times a particular colour is eliminated - the higher the count the harder the problem since it requires more iteration of the rules to solve. (A counter example to this would be a board with 1 colour covering everything except the cells a queen of the other colours needs to be placed on)
Also I'm trying to evaluate the efficacy of performing colour swaps but it's proving more challenging than I thought. The basic idea is you can swap the colours of neighbouring cells to line up multiple colours so there are less obvious "single cells" which contains the queen. The problem with this is it can introduce other solutions and it's difficult to tell whether a swap makes the puzzle harder or simpler to solve.
Conceptually they are similar, but the math is way over my head. I have trouble grokking each one actually.
But it's pretty easy for a beginner to start with a list of true/false (or true/null) monads as inputs to a pure function. Imagine the monads occupying nodes in a tree structure like JSON, or merging through NAND/NOR gates to reduce to fewer outputs.
From the outside, we can toggle the inputs to feed them examples like 0101 and see how that affects the outputs. This is basically how a spreadsheet works.
Then we can extend the monads to contain a set of values. Or even a range of values, like a floating point number from 0 to 1 or 0 to pi/2, etc, more like imaginary numbers for use in quantum programming (not sure if this is still a monad).
Functional programming can lazily evaluate the inputs and eliminate don't-cares to calculate all possible outputs within the limits of their computing power and time. Quantum gates can do something similar using the interference patterns between the inputs and logic somehow (the hand wavy part nobody seems to be able to explain).
Maybe this approach could be used as a bridge to eliminate the hand wavy part and give us something tractable in layman's terms. This might be considered quantized or simulated quantum programming.
-
Note: monads are similar to futures/promises and async/await in imperative programming, like using the imaginary number i in algebra. Except that we are generally only concerned with a handful of expected results, so often miss the failure modes by not stress-testing the logic with fuzzing and similar techniques. Which tends to make async code nondeterministic and brittle. So I'm also interested in transpiling async/nonblocking <-> sync/blocking and state machine <-> coroutine.
Clean, thoughtful, and practical. Curious, have you tried benchmarking your Haskell solver against an SMT solver (like Z3 or CVC5) to compare performance or expressiveness?
I'm curious how this would look using an exact covering algorithm. I'm also vaguely curious to see the various solutions that have been explored lately benchmarked. For that matter, a table that gives the stats on the code and execution would almost certainly lead to some amusing fights.
Hmm, an interesting pattern is that every queen is a knight's move away. I haven't thought about this problem since I started dabbling in chess but now looks like a simple pattern.
how would you encode a constraint system where the generator must yield exactly one solution and that solution remains unique under all transformations in the problem’s symmetry group, without relying on post-solution filtering or external isomorphism checks?
Directly modelling the unique solution property would be a quantified problem, essentially it would be "there exists a solution such that it is not the case that there exists a different solution". In principle, you can explode this into an enumeration of all O(n!) placements of queens and saying "either the placement is the same as the solution, or it is not a solution". That significantly increases the model size though.
For the symmetry, LinkedIn Queens generally do not have symmetric boards since that would imply more than one solution.
A simpler approach uses mixed-integer LP (MIP) and a mathematical programming DSL like julia/JuMP or python/pyomo.
Here's a trivial and fast MIP solution using python/pulp, which would be essentially the same in any mathematical programming DSL:
from collections import defaultdict
import pulp
board = [
["P", "P", "P", "P", "P", "P", "P", "P", "P"],
["P", "P", "R", "S", "S", "S", "L", "L", "L"],
["P", "R", "R", "W", "S", "L", "L", "L", "L"],
["P", "R", "W", "W", "S", "O", "O", "L", "L"],
["P", "R", "W", "Y", "Y", "Y", "O", "O", "L"],
["P", "R", "W", "W", "Y", "O", "O", "L", "L"],
["P", "R", "R", "W", "Y", "O", "B", "L", "L"],
["P", "R", "R", "G", "G", "G", "B", "B", "L"],
["P", "P", "R", "R", "G", "B", "B", "L", "L"],
]
# group by color for color constraint
def board_to_dict(board):
nr = len(board)
res = defaultdict(list)
for i, row in enumerate(board):
if len(row) != nr:
raise ValueError("Input must be a square matrix")
for j, color in enumerate(row):
res[color].append((i, j))
return res
color_regions = board_to_dict(board)
N = len(color_regions)
prob = pulp.LpProblem("Colored_N_Queens", pulp.LpMinimize)
x = [[pulp.LpVariable(f"x_{i}_{j}", cat="Binary") for j in range(N)] for i in range(N)]
# Row constraints
for i in range(N):
prob += pulp.lpSum(x[i][j] for j in range(N)) == 1
# Column constraints
for j in range(N):
prob += pulp.lpSum(x[i][j] for i in range(N)) == 1
# Color region constraints
for positions in color_regions.values():
prob += pulp.lpSum(x[i][j] for (i, j) in positions) == 1
# No diagonal adjacency
for i in range(N):
for j in range(N):
for di, dj in [(-1, -1), (-1, 1), (1, -1), (1, 1)]:
ni, nj = i + di, j + dj
if 0 <= ni < N and 0 <= nj < N:
prob += x[i][j] + x[ni][nj] <= 1
# Trivial objective
prob += 0
res = prob.solve()
print(f"Solver status: {pulp.LpStatus[prob.status]}")
if pulp.LpStatus[prob.status] == "Optimal":
for i in range(N):
row = ""
for j in range(N):
row += ("#" if pulp.value(x[i][j]) > 0.5 else " ") + board[i][j] + " "
print(row)
and its output:
#P P P P P P P P P
P P R S S #S L L L
P R R W S L L L #L
P R #W W S O O L L
P R W Y Y Y O #O L
P R W W #Y O O L L
P #R R W Y O B L L
P R R #G G G B B L
P P R R G B #B L L
Reminds me of this classic: https://aphyr.com/posts/342-typing-the-technical-interview
As a professional haskeller, I feel it necessary to point out for people in this thread who are less exposed to Haskell and who may be Haskell-curious...this is not what real-world commercial Haskell code looks like. To use a C analogy, I'd say it's closer to IOCCC entries than Linux kernel code.
Thanks for that. Having read the article, I was left with the overwhelming impression that I'd have solved it in a totally different way if I was trying in OCaml.
Briefly, I'd have started with an array which for each colour had an array containing the coordinate pairs for that colour. I'd probably then have sorted by length of each array. The state also has an empty array for the coordinates of each placed queen.
To solve, I'd take the head array as my candidates, and the remaining array of arrays as the next search space. For each candidate, I'd remove that coordinate and anything that was a queen move from it from the remaining arrays, and recursively solve that. If filtering out a candidate coordinate results in an empty list for any of the remaining arrays, you know that you've generated an invalid solution and can backtrack.
At no point would I actually have a representation of the board. That feels very imperative rather than functional to me.
To me, this solution immediately jumps out from the example - one of the queens in on a colour with only 1 square, so it HAS to be there. Placing that there immediately rules out one of the choices in both colours with 2 squares, so their positions are known immediately. From that point, the other 2 large regions have also been reduced to a single candidate each.
Yeah, comparing to how you'd solve this in any other mainstream language is really an apples-to-oranges comparison here because this is explicitly tackling the contrived problem of solving it at the type level rather than at the much more common value level. Very few languages in existence have the ability to do this kind of type-level computation. I'd say Haskell is really the only language that could conceivably be called "viable for mainstream use" that currently supports it, and even in Haskell's case the support is new, largely experimental, in a state of active research, and not well integrated with the ergonomics of the rest of the language.
As someone who has never touched Haskell and who knows nearly nothing about it, Haskell is not, in fact, a "dynamically typed, interpreted language", which, "has no currying".
At the risk of explaining away a perfectly good joke, that person is writing programs at the type level. The joke is that the type system is turing complete if you enable the right extensions.
This gives me a message "Unavailable Due to the UK Online Safety Act" which sounds like nonsense for a blog post, but IANAL. Can anyone summarise the post, or suggest why there'd be a reason my online safety is compromised by it?
It's pretty clear that the issue is not the post, but the fact that you are in UK, and the site author does not deem you important enough.
The site author himself has blocked users from the UK because of that stupid law that you cite in your comment: "The UK's Online Safety Act requires operators of 'user to user services' to read through hundreds (if not thousands) of pages of documentation to attempt to craft "meaningful" risk assessments and 'child access assessments' or face £18,000,000 fines, even imprisonment."
Here you go: https://web.archive.org/web/20250213135223/https://aphyr.com...
A thing of beauty! Was going to post the same.
related:
- with SMT (11 days ago, 47 comments) https://news.ycombinator.com/item?id=44259476
- with APL (10 days ago, 1 comment) https://news.ycombinator.com/item?id=44273489 and (8 days ago, 20 comments) https://news.ycombinator.com/item?id=44275900
- with MiniZinc (1 day ago, 0 comment) https://news.ycombinator.com/item?id=44353731
- with SAT (27 days ago, 1 comment) https://news.ycombinator.com/item?id=44115866
I set this as part of a Scala programming assignment for my second year undergraduate class at UNE (Australia) last term. However, during the working a square is not Queen | Eliminated but Set[Queen | NotQueen]
Largely so from a programming perspective it becomes a simplified version of Einstein's Riddle that I showed the class, doing in a similar way.
https://theintelligentbook.com/willscala/#/decks/einsteinPro...
Where at each step, you're just eliminating one or more possibilities from a cell that starts out containing all of them.
Queens has fewer rules to code, making it more amenable for students.
thanks for saying this, that is how I play this game usually, and I was confused by TFA going with backtracking/guessing a next attempt, when constraint propagation seems easier, I thought I was missing something.
Solving Queens using J and brute force all permutations.
Just when I start thinking I am smart, someone drops this :) Haskell certainly looks graceful but is imposing! I feel pretty good if I can do functional stuff in Rust, but this is next level.
I think it's helpful to separate out the "Haskell is imposing" from "This language that I don't know is imposing". It is unrealistic to expect to be able to read a language you don't know. It is easy to be accidentally trained otherwise, because there are several languages out there that are hardly different from each other except in unimportant details and in a perfect world perhaps we wouldn't need both of them, and if you work with a couple of them you might get used to being able to read across languages, but those are really the exceptions rather than the rule. Even if they are very, very large and popular exceptions.
I won't say this reduces the "Haskell is imposing" to zero, but a non-trivial amount of the initial impression of imposingness is just the very different syntax, such as the way functions are not called with parentheses after the function name. But the different syntax isn't really that big a deal. You just don't know it and aren't used to it. Under the hood it does have some differences, but the differences are magnified when you try to swallow the surface differences and the deep differences all in one shot. Nobody who knows Haskell did that; they learned it the same way you learn any other language, one bit at a time.
You should write a "Solving LinkedIn Queens with Rust" post :)
I believe I first encountered this problem while working through SICP. Was confused why it's called Linkedin queens, since this problem is a classical one in CS that definitely pre-dated the existence of Linkedin.
LinkedIn's daily Queens puzzle is different than the classical problem in two ways: it adds colored regions which also must have exactly one queen, and it relaxes the diagonal constraint -- queens are allowed in the same diagonal as long as they are not adjacent.
Does anyone know of any algorithms for generating these game boards ?
That will produce challenging boards ?
It's a hard problem, for a bunch of reasons :)
1) It's not too hard to make a problem with at least one solution (just put the queens down first, then draw boxes), but there isn't any good way of making levels with unique solutions.
2) Once you've accomplished that, it's hard to predict how hard a level will be, and then it's hard to make levels easier / harder.
I happen to be currently researching this topic (well, I'm doing all kinds of these grid-based puzzles, but this is an example). The algorithm tries to make "good" levels, but there is a good probability it will end up with something useless we need to throw away, and then try again.
It's easy to make levels which are trivial, and similarly easy to make levels which are far beyond human ability, but hitting things in the 'human tricky but solvable' sweet-spot is where most of the difficulty comes from.
I should probably try writing up a human-readable version of how I do it. It involves a bunch of Rust code, so I can hit a whole bunch of trendy topics!
> I should probably try writing up a human-readable version of how I do it. It involves a bunch of Rust code, so I can hit a whole bunch of trendy topics!
Do you have a blog? I'm interested.
Given that this could be a variant of "exact cover", using zdds to explore the problem space might simplify finding exact puzzles in addition to puzzles that require lookahead.
Generally what is needed is a subroutine that can tell you 1) if the problem has a solution, and 2) if the solution is unique (common requirement for puzzles like these). Using such a model as a sub-routine, a heuristic search can be done to gradually build up puzzles. If your solver technology of choice can handle quantified problems, that could be used to integrate those two problems into one, but that is quite a lot harder to to.
If the base solver you have is a system that can be run in various configurations with different levels of reasoning and assumption as well as a report on the amount of search needed if any, that can be very useful as a way to measure the hardness. In Sudoku as a Constraint problem (https://citeseerx.ist.psu.edu/document?doi=4f069d85116ab6b4c...), Helmut Simonis tested lots of 9x9 Sudoku puzzles against various levels of propagation and pre-processing as a way to measure the hardness of Sudoku puzzles by categorizing them by the level of reasoning needed to solve without search. The MiniZinc model for LinkedIn Queens (https://news.ycombinator.com/item?id=44353731) can be used with various solvers and levels of propagation as such a subroutine.
Now, for production-level puzzle making, such as what King does for Candy Crush, the problems and requirements are even harder. I've heard presentation where they talk about training neural networks to play like human testers, so not optimal play but most human like play, in order to test the hardness level of the puzzles.
It's the same problem as with generating good sudoku boards. It's not easy, and there's not many publicly available solutions, but solutions exist.
A common opinion is that a good board is solvable without the use of backtracking. A set of known techniques should be enough to solve the board. To validate if a board is "fun" you need to have a program that can solve the board using these known techniques. Making that program is much harder than just making a general solver. And then you need to find the boards that can be validated as fun. Either you search through random boards, or you get clever...
I've noticed that puzzles that can be solved with CP-SAT's presolver so that the SAT search does not even need to be invoked basically adhere to this (no backtracking, known rules), e.g.:
Together with validating that there is only 1 solution you would probably be able to make the search for good boards a more guided than random creation.Simulated annealing with a difficulty heuristic (like minimum required logical steps) works well - start with a valid solution, then randomly modify colors while maintaining uniqueness.
Awesome, I'm writing a "logical solver" just like this - I'll hopefully also have something to post here when I'm done.
I'm trying to use it during the generation process to evaluate the difficulty a basic heuristic I'm trying to work with is counting the number of times a particular colour is eliminated - the higher the count the harder the problem since it requires more iteration of the rules to solve. (A counter example to this would be a board with 1 colour covering everything except the cells a queen of the other colours needs to be placed on)
Also I'm trying to evaluate the efficacy of performing colour swaps but it's proving more challenging than I thought. The basic idea is you can swap the colours of neighbouring cells to line up multiple colours so there are less obvious "single cells" which contains the queen. The problem with this is it can introduce other solutions and it's difficult to tell whether a swap makes the puzzle harder or simpler to solve.
Does anyone know of a way to transpile monadic logic to quantum logic?
https://en.wikipedia.org/wiki/Monad_(functional_programming)
https://en.wikipedia.org/wiki/Quantum_programming
Conceptually they are similar, but the math is way over my head. I have trouble grokking each one actually.
But it's pretty easy for a beginner to start with a list of true/false (or true/null) monads as inputs to a pure function. Imagine the monads occupying nodes in a tree structure like JSON, or merging through NAND/NOR gates to reduce to fewer outputs.
From the outside, we can toggle the inputs to feed them examples like 0101 and see how that affects the outputs. This is basically how a spreadsheet works.
Then we can extend the monads to contain a set of values. Or even a range of values, like a floating point number from 0 to 1 or 0 to pi/2, etc, more like imaginary numbers for use in quantum programming (not sure if this is still a monad).
Functional programming can lazily evaluate the inputs and eliminate don't-cares to calculate all possible outputs within the limits of their computing power and time. Quantum gates can do something similar using the interference patterns between the inputs and logic somehow (the hand wavy part nobody seems to be able to explain).
Maybe this approach could be used as a bridge to eliminate the hand wavy part and give us something tractable in layman's terms. This might be considered quantized or simulated quantum programming.
-
Note: monads are similar to futures/promises and async/await in imperative programming, like using the imaginary number i in algebra. Except that we are generally only concerned with a handful of expected results, so often miss the failure modes by not stress-testing the logic with fuzzing and similar techniques. Which tends to make async code nondeterministic and brittle. So I'm also interested in transpiling async/nonblocking <-> sync/blocking and state machine <-> coroutine.
Clean, thoughtful, and practical. Curious, have you tried benchmarking your Haskell solver against an SMT solver (like Z3 or CVC5) to compare performance or expressiveness?
Thanks. Yes, there are comparisons with Z3 towards the end of the post.
I don't think expressiveness applies here.
I'm curious how this would look using an exact covering algorithm. I'm also vaguely curious to see the various solutions that have been explored lately benchmarked. For that matter, a table that gives the stats on the code and execution would almost certainly lead to some amusing fights.
Kinda off topic but I had some much fun solving n queens in SQL: https://gist.github.com/seisvelas/952185983a625cd16e1ed4d901...
Hmm, an interesting pattern is that every queen is a knight's move away. I haven't thought about this problem since I started dabbling in chess but now looks like a simple pattern.
Only for that particular board, in general it will be very complex and depend on the shape of the colored regions
Solving Queens in J from a novice J programmer:
how would you encode a constraint system where the generator must yield exactly one solution and that solution remains unique under all transformations in the problem’s symmetry group, without relying on post-solution filtering or external isomorphism checks?
Directly modelling the unique solution property would be a quantified problem, essentially it would be "there exists a solution such that it is not the case that there exists a different solution". In principle, you can explode this into an enumeration of all O(n!) placements of queens and saying "either the placement is the same as the solution, or it is not a solution". That significantly increases the model size though.
For the symmetry, LinkedIn Queens generally do not have symmetric boards since that would imply more than one solution.
[dead]
So you're the co-worker playing Queens according to my LinkedIn notifications!
That's probably Ryan Berger. They have a Firefox extension: https://ryanberger.me/posts/queens/
Anything similar with Zip? That's the one I enjoy in the mornings.
That's going to be much harder for sure
A simpler approach uses mixed-integer LP (MIP) and a mathematical programming DSL like julia/JuMP or python/pyomo.
Here's a trivial and fast MIP solution using python/pulp, which would be essentially the same in any mathematical programming DSL:
and its output:[dead]
Have not done part 2 but enjoyed the first part of the course!
Just started part 2 last week! It’s really one of the best moocs I’ve done.