Re:Solving LinkedIn Queens with SMT
by cpatuzzo on Thursday June 12, 2025 @02:27PM
(#44261126)
I tried to write a programming language that compiles to SAT many years ago: https://sentient-lang.org/
[ Parent
| on HN ]
I remember you showing me this! Wow that was a long time ago.
Re:Solving LinkedIn Queens with SMT
by superlopuh on Friday June 13, 2025 @05:15AM
(#44266983)
I love that language and frequently show it to people. I'm sad to see that my local install doesn't work any more. I actually used it to solve a puzzle in Evoland 2 that I'm relatively sure was added as a joke, and is not solvable in a reasonable time without a solver. I'm actually doing a PhD in compilers right now, and would love to chat about sentient if you have the time. My email is [email protected].
You might be interested in looking at MiniZinc (https://minizinc.org/) which is an open source modelling language for combinatorial problems. The system comes from a constraint programming background but the language is solver agnostic can be used to compile into many different types of solvers.