Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A dumb introduction to z3

asibahi.github.io

Post reply on HN
Print view View original

11–20 of 42 posts

Re: A dumb introduction to z3

#11

Post by zdance »

cube2222 wrote: post #4

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”?…

37 is irreducible in the problem statement, so the answer is 37.

Think about it purely in the set-theoretic sense "what is the minimal set containing 37 elements?" the answer is "the set containing 37 elements."

Re: A dumb introduction to z3

#12

Post by [deleted] »

cube2222 wrote: post #4

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”?…

[deleted]

Re: A dumb introduction to z3

#13

Post by metadat »

pkoird wrote: post #6
sophacles wrote: post #3

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.

Going one abstraction deeper, SAT solvers are black magic.

Yes, explaining the "why / how did the SAT solver produce this answer?" can be more challenging than explaining some machine learning model outputs.

You can literally watch as the excitement and faith of the execs happens when the issue of explainability arises, as blaming the solver is not sufficient to save their own hides. I've seen it hit a dead end at multiple $bigcos this way.

Re: A dumb introduction to z3

#14

Post by Dylan16807 »

zdance wrote: post #11
cube2222 wrote: post #4

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”?…

37 is irreducible in the problem statement, so the answer is 37. Think about it purely in the set-theoretic sense "what is the minimal set containing 37 elements?" the answer is "the set containing 37 elements."

The fixed 37 is the value of the coins. It's very easy to reduce the number of coins.

Either you misunderstood something or please explain more. Note that both the working and broken versions have the same 37 in them.

And the problem statement starts with no coins chosen. It had to actively choose pennies to get that broken result. If you told it about the coins in a different order, it probably would have given a different answer.

Re: A dumb introduction to z3

#16

Post by almostgotcaught »

sophacles wrote: post #3

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.

The solution is to look at a lot of examples

https://www.hakank.org/

Re: A dumb introduction to z3

#18

Post by QuadmasterXLII »

joek1301 wrote: post #10

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

I guess z3 is fine with it, but it confuses me that they decided pips wouldn't have unique solutions

Re: A dumb introduction to z3

#19

Post by adsharma »

Those of you wondering about how to use z3, please consider coding in static python (not z3py) and then transpile to smt2.

You'll be able to solve bigger problems with familiar/legible syntax and even use the code in production.

Re: A dumb introduction to z3

#20

Post by weinzierl »

The way you can write code of the target DSL without wrapping it in a string both gives me fears and excitement:

    solver.assert((&x + 4).eq(7));
My subconsciousness shouts "MISSING QUOTES" while my ratio says "Calm down, that's nice and clean and safe and how it's supposed to be - ever has been".
Post reply on HN