Prolog nezmizel. Jeho hlavní myšlenku dnes potkáváme v nástrojích, které se Prologu na první pohled nepodobají: v CodeQL pro analýzu kódu, v Rego pro policy-as-code, v Z3 pro práci s omezeními a v Leanu pro formální důkazy. Každý řeší jiný problém, ale všechny připomínají totéž: někdy je lepší popsat vztahy, pravidla, omezení nebo tvrzení než vrstvit další if.
https://zdrojak.cz/clanky/prolog-nezmizel-jen-dnes-zije-v-jinych-nastrojich/
Today's in-the-wild carspotting: a really well-kept Z3.
For this one part 1 was relatively simple (parsing was the longest task), despite my basic bruteforce solution still needing more than 2s to find an answer.
For part 2 I was initially excited to finally implement Gaussian elimination by myself, but then realized it couldn't work because this was a minimization problem. A quick search showed me that it was an integer linear programming problem, which everyone recommended to solve with a library.
Despite my better judgement, I convinced myself that a DFS exploration could maybe work. And it did! ... on the example.
So in the end I caved and did it with z3 like most people. At least it seems that the z3 crate has greatly improved in the past 2 years, and my code using it is relatively simple.
I also found this fun thing on the Z3 C documentation: https://social.treehouse.systems/@Aissen/115699422672481929
Advent of Code is an Advent calendar of small programming puzzles. I participated in this year's edition, finishing it for the second time in row. The puzzles of all editions are always accessible. The principle is to read the problem, get a puzzle input (more or less tailored to your …
Advent of Code 2025 Day 10: Factory
This is the one where I started with BFS and ended with Z3. WTF is Z3?
https://westkarana.blog/2025/12/10/advent-of-code-2025-day-10-factory/
I've completed "Factory" - Day 10 - Advent of Code 2025
I used Z3 to solve Part 2 in ~500ms. I still need to clean up Part 1's brute force.
https://github.com/jstanden/advent-of-code-python/blob/main/2025/day10.ipynb
It’s that time of the year again - someone (me) wanting to try replacing #gentoo ‘s #portage with a #Z3 #SMT solver. Well, this time I did it! Or at least started to… got 2x performance boost but it’s not quite black and white.
https://blog.researchmonger.com/2025/12/integrating-z3-smt-solver-into-gentoo.html?m=1
Zdroják
Liam O'Mara IV, PhD
Donald Ham 
Patrick 
Anisse
Tipa
Jeff Standen
Hexorg
José A. Alonso