frontpage.
newsnewestaskshowjobs

Made with ♥ by @iamnishanth

Open Source @Github

fp.

Open in hackernews

A dumb introduction to z3

https://asibahi.github.io/thoughts/a-gentle-introduction-to-z3/
63•kfl•1d ago

Comments

throwaway81523•1h ago
This is good too: https://yurichev.com/writings/SAT_SMT_by_example.pdf
pkoird•1h ago
imo this is the pdf that many people like me used to learn SAT/SMT.
sophacles•1h ago
Constraint solvers are a cool bit of magic. The article underplays how hard it is to model problems for them, but when you do have a problem that you can shape into a sat problem... it feels like cheating.
pkoird•1h ago
Going one abstraction deeper, SAT solvers are black magic.
mikestorrent•29m ago
If you're good at doing this, you should check out the D-Wave constrained quadratic model solvers - very exciting stuff in terms of the quality of solution it can get in a very short runtime on big problems.
ngruhn•18m ago
I took a course on SMT solvers in uni. It's so cool! They're densely packed with all these diverse and clever algorithms. And there is still this classic engineering aspect: how to wire everything up, make it modular...
cube2222•1h ago
I’d be curious if someone here could explain the initial nonsensical answer for the coin change problem.

I understand that not giving the lower bounds effectively lets it find an arbitrarily low (generally very negative) number of coins that satisfy the problem (so the minimization would basically go to negative infinity).

But why would it respond with “to get 37 in the lowest number of coins I’ll give you 37 ones”?

Or is this kind of like “if the answer to your minimization problem is negative infinity, the answer is undefined behavior”?

gopalv•21m ago
> is this kind of like “if the answer to your minimization problem is negative infinity, the answer is undefined behavior”?

Yes, it picked a valid result and gave up.

I got a similar nonsensical result in my run-ins[1] in with SAT solvers too, until I added a lowerbound=0.

The "real life" follow-up question in interviews was how to minimize the total number of intermediate rows for a series of joins within in a cost-based optimizer.

[1] - https://gist.github.com/t3rmin4t0r/44d8e09e17495d1c24908fc0f...

joek1301•2m ago
I also was inspired to play around with Z3 after reading a Hillel Wayne article.

I used it to solve the new NYT game, Pips: https://kerrigan.dev/blog/nyt-pips

Shai-Hulud malware attack: Tinycolor and over 40 NPM packages compromised

https://www.stepsecurity.io/blog/ctrl-tinycolor-and-40-npm-packages-compromised
777•jamesberthoty•11h ago•608 comments

How to make the Framework Desktop run even quieter

https://noctua.at/en/how-to-make-the-framework-desktop-run-even-quieter
152•lwhsiao•4h ago•35 comments

Things you can do with a Software Defined Radio (2024)

https://blinry.org/50-things-with-sdr/
534•mihau•8h ago•102 comments

Denmark close to wiping out cancer-causing HPV strains after vaccine roll-out

https://www.gavi.org/vaccineswork/denmark-close-wiping-out-leading-cancer-causing-hpv-strains-aft...
388•slu•4h ago•154 comments

Waymo has received our pilot permit allowing for commercial operations at SFO

https://waymo.com/blog/#short-all-systems-go-at-sfo-waymo-has-received-our-pilot-permit
505•ChrisArchitect•6h ago•484 comments

A dumb introduction to z3

https://asibahi.github.io/thoughts/a-gentle-introduction-to-z3/
63•kfl•1d ago•9 comments

I built my own phone because innovation is sad rn [video]

https://www.youtube.com/watch?v=qy_9w_c2ub0
139•Timothee•1d ago•28 comments

How Container Filesystem Works: Building a Docker-Like Container from Scratch

https://labs.iximiuz.com/tutorials/container-filesystem-from-scratch
77•lgunsch•3d ago•15 comments

Wind turbine blade transportation challenges

https://spectrum.ieee.org/wind-turbine-blade-transport-plane
67•Brajeshwar•3d ago•80 comments

A new experimental Google app for Windows

https://blog.google/products/search/google-app-windows-labs/
110•meetpateltech•8h ago•151 comments

Launch HN: Rowboat (YC S24) – Open-source IDE for multi-agent systems

https://github.com/rowboatlabs/rowboat
42•segmenta•6h ago•22 comments

Should We Drain the Everglades?

https://rabbitcavern.substack.com/p/should-we-drain-the-everglades
53•ksymph•3h ago•35 comments

SQL performance improvements: finding the right queries to fix

https://ohdear.app/news-and-updates/sql-performance-improvements-finding-the-right-queries-to-fix...
11•freekmurze•2h ago•0 comments

The "Most Hated" CSS Feature: Cos() and Sin()

https://css-tricks.com/the-most-hated-css-feature-cos-and-sin/
24•rapawel•2h ago•17 comments

Scammed out of $130K via fake Google call, spoofed Google email and auth sync

https://bewildered.substack.com/p/i-was-scammed-out-of-130000-and-google
236•davidscoville•6h ago•417 comments

Plugin System

https://iina.io/plugins/
122•xnhbx•6h ago•31 comments

When the job search becomes impossible

https://www.jeffwofford.com/wp/?p=2240
126•pertinhower•9h ago•142 comments

Micro-LEDs boost random number generation

https://discovery.kaust.edu.sa/en/article/25936/micro-leds-boost-random-number-generation/
5•giuliomagnifico•1h ago•0 comments

UTF-8 history (2003)

https://doc.cat-v.org/bell_labs/utf-8_history
82•mikecarlton•3d ago•31 comments

The Linux Process Journey (2023) [pdf]

https://thelearningjourneyebooks.com/wp-content/uploads/2023/09/TheLinuxProcessJourney_v6_Sep2023...
45•maxmoehl•5h ago•1 comments

Writing an operating system kernel from scratch – RISC-V/OpenSBI/Zig

https://popovicu.com/posts/writing-an-operating-system-kernel-from-scratch/
79•popovicu•2d ago•3 comments

CIA Freedom of Information Act Electronic Reading Room

https://www.cia.gov/readingroom
141•bookofjoe•9h ago•32 comments

Paper Folding Assembly Line [video]

https://www.youtube.com/watch?v=XhUuhl9iWpQ
53•peteforde•1w ago•8 comments

Top UN legal investigators conclude Israel is guilty of genocide in Gaza

https://www.middleeasteye.net/news/un-concludes-israel-guilty-genocide-gaza
535•Qem•14h ago•327 comments

Bertrand Russell to Oswald Mosley (1962)

https://lettersofnote.com/2016/02/02/every-ounce-of-my-energy/
164•giraffe_lady•6h ago•80 comments

Implicit ODE solvers are not universally more robust than explicit ODE solvers

https://www.stochasticlifestyle.com/implicit-ode-solvers-are-not-universally-more-robust-than-exp...
92•cbolton•9h ago•29 comments

Development of the MOS Technology 6502: A Historical Perspective (2022)

https://www.EmbeddedRelated.com/showarticle/1453.php
52•jason_s•8h ago•8 comments

60 years after Gemini, newly processed images reveal details

https://arstechnica.com/space/2025/09/60-years-after-gemini-newly-processed-images-reveal-incredi...
250•sohkamyung•3d ago•70 comments

Soviet Maps (2021)

https://twitter.com/LindyScience/status/1413532678318612482
25•georgecmu•3d ago•4 comments

Generative AI as Seniority-Biased Technological Change

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=5425555
199•zeuch•9h ago•172 comments