#z3 — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #z3, aggregated by home.social.
-
Today's in-the-wild carspotting: a really well-kept Z3.
-
One Open-source Project Daily
The Z3 Theorem Prover
https://github.com/Z3Prover/z3
#1ospd #opensource #z3 -
CW: AoC day 10: Factory
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 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
-
Readings shared December 5, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/06-readings_shared_12-05-25 #ATP #Autoformalization #DataScience #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Rocq #Rstats #SMT #Z3
-
Automated Reasoning For Uncertain Markov Processes ~ Muhammad Maaz. https://utoronto.scholaris.ca/server/api/core/bitstreams/e3196e4a-69ca-4e3d-9932-66ea3cb35232/content #ATP #SMT #Z3
-
Reconstruction of Konrad Zuse's Z3 Computer
https://dcmlr.inf.fu-berlin.de/rojas/index.html%3Fp=560.html
#HackerNews #Reconstruction #Zuse #Z3 #Computer #Technology #History #ComputerScience
-
In this world-shattering revelation, we're led through the riveting journey of solving #Sudoku with #Rust and #z3, because apparently, life wasn't complicated enough already. 🤯✨ The author bravely tackles the arcane realm of constraint solvers, all while serving us the hottest take: complicated problems can be, wait for it... complicated. 🥱🔍
https://asibahi.github.io/thoughts/a-gentle-introduction-to-z3/ #ConstraintSolvers #TechHumor #Complexity #HackerNews #ngated -
A Dumb Introduction to z3 using Rust
https://asibahi.github.io/thoughts/a-gentle-introduction-to-z3/
#HackerNews #A #Dumb #Introduction #to #z3 #using #Rust #z3 #Rust #Programming #Education #Tech
-
Back on the ol' #Z3 for laying out the schedule for @ParslProject annual conference. Slightly overkill but manual scheduling was also slightly too hard.
-
A few months ago I tried to write a Binate Covering Problem (BCP) solver, and haven't yet gotten it working.
But today I realized that writing one is a waste of time. BCP can be solved by a Max-SAT solver, and a huge amount of effort has been invested by very smart people to make those work efficiently. My feeble attempt at a BCP solver couldn't possibly do better.
Here's Python code to solve BCP using Z3's Python bindings:
https://github.com/brouhaha/bcp-z3-python
#BCP #BinateCoveringProblem #SAT #Z3 -
Kevin Sahr DGGRID 8.41 was released, with full support for #IGEO7 #Z7 #ZORDER and #Z3 indexing for #ISEA 3,4 and 7 H #DGGS the binaries on conda-forge are updated. And we are now testing HTML readme/docs:
https://github.com/sahrk/DGGRID/releases
-
[Перевод] Решаем задачу про ферзей при помощи SMT-солвера
Автор статьи Modern SAT solvers: fast, neat and underused утверждает, что SAT-солверы «преступно мало используются в нашей отрасли». [SAT — Boolean SAT isfiability Solver, то есть солвер, способный находить присвоения, делающие истинными сложные булевы выражения. Более подробно я писал о них ранее.] Какое-то время назад я задался вопросом, почему: как получилось, что они настолько мощны, но ими никто не пользуется? Многие специалисты заявили, что причина в неудобстве кодирования SAT: они лучше предпочтут работать с инструментами, которые выполняют компиляцию в SAT. Я вспомнил об этом, когда прочитал пост Райана Бергера о решении «задачи ферзей с LinkedIn» как задачи SAT. Вкратце опишу задачу про ферзей (Queens). У нас есть сетка NxN, разделённая на N областей, и нам нужно разместить N ферзей так, чтобы в каждом столбце, строке и области находился ровно один. Ферзи могут находиться на одной диагонали, но не соседствовать по диагонали.
-
Z3Guide: A scalable, student-centered, and extensible educational environment for logic modeling. ~ Ruanqianqian Huang, Ayana Monroe, Peli de Halleux, Sorin Lerner, Nikolaj Bjørner. https://arxiv.org/abs/2506.08294v1 #Logic #SMT #Z3 #Teaching
-
Ein #Relaisrechner in Aktion zum 115. #Zuse-Geburtstag
#Computer ohne Bildschirm, Maus oder Tastatur, wie funktionierte das überhaupt? Zum 115. #Geburtstag von #KonradZuse zeigt das #ZCOM am Sonntag, den 22.06.2025 ab 13 Uhr im Rahmen der Reihe „Anfassen & Verstehen“ ein funktionsfähiges Modell eines #historischen #Relaisrechners. Mit Klicks, Klacken und Kontaktfedern wird erlebbar, wie #Zuse seine bahnbrechende #Z3 entwickelte und damit einen Grundstein für unsere...
-
Ein #Relaisrechner in Aktion zum 115. #Zuse - #Geburtstag:
#Computer ohne Bildschirm, Maus oder Tastatur, wie funktionierte das überhaupt? Zum 115. Geburtstag von #KonradZuse zeigt das #ZCOM am Sonntag, den 22.06.2025 ab 13 Uhr im Rahmen der Reihe „Anfassen & Verstehen“ ein funktionsfähiges Modell eines #historischen #Relaisrechners. Mit Klicks, #Klacken und #Kontaktfedern wird erlebbar, wie #Zuse seine #bahnbrechende #Z3 entwickelte und damit einen Grundstein...
-
It seems like the #TimeOfFlowers #season has barely begun and I'm already hopelessly behind on sharing photos! Things move fast at this time of year, new things opening every day or so, previous waves of flowering wrapping up.. These are from 10 days ago, some finished or on the way out.. White Draba dedeana Yellow Draba aizoides and D. bruniifolia ssp olympica. Tulipa urumiensis (or something..) #garden #RockGarden #spring #NaturalGardening #Alberta #Canada #z3
-
Vor 84 Jahren – am 11. Mai 1941 – hat Konrad #Zuse in Zusammenarbeit mit Helmut #Schreyer die #Z3 vollendet, den ersten funktionsfähigen, frei programmierbaren Rechner der Welt. Perfekt umgesetzt: #AirGap by Design, #ZeroTrust durch Einzelzugriff, keine Cloud, kein Netzwerk, kein Admin-Account. 🙂
-
SAT-solving the poset cover problem. ~ Chih-Cheng Rex Yuan, Bow-Yaw Wang. https://arxiv.org/abs/2505.04013 #ATP #SAT_solvers #Z3
-
The inner magic behind the Z3 theorem prover - Microsoft Research (October 2019):
https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/
-
Long Hei Matthew Lam from Monash University has given the oral presentation titled A Closer Look at Tool-based Logical Reasoning with #LLMs: The Choice of Tool Matters.
In this paper, he fills the gaps in the comparison between symbolic solvers, including #Z3, #Pyke, and
#Prover9 with #LLMs augmented. -
I recently read a paper by Kleshnina and others and used it to teach myself some evolutionary game theory techniques.
This is a little obscure, so I'll thread below about why this topic matters for humans and the environment 🧵
https://nadiah.org/2024/11/20/kleshnina_2023
#GameTheory #PrisonersDilemma #iteratedGame #cooperation #EvolutionOfCooperation #Z3 #pyeda #networkx #sympy #SageMath #sustainability
-
Lecturas compartidas el 7 de junio de 2024. https://jaalonso.github.io/vestigium/posts/2024/06/08-lecturas_compartidas_el_07-jun-24 #ITP #Lean4 #IsabelleHOL #PVS #Math #ATP #Prover9 #SMT #Z3 #FunctionalProgramming #Haskell #LLMs
-
Heute vor 80 Jahren führten Konrad Zuse und Helmut Schreyer den ersten frei programmierbaren und programmgesteuerten Rechenautomaten vor. Vor 80 Jahren: Konrad Zuses Computer Z3 läuft
