thank you so much :) this explanation really helped me to get a basic intuition for using z3. I'm working on a thesis which deals with tree-structured test data generation and my first strategy was to use smt solvers like z3 to drive the generating process, but I got a bit lost while trying to understand the smt-lib format.

Man what amazing explanation should have 1 million views, thx a lot, and go ahead with channel

WOW!!! incredible explanation, the only reason you didn't get more views is because you didn't fill your house up with jello and scream at everyone that "you are filling your house up with jello", then change your camera angles every 2 seconds with the added random noises from manga characters.

@HackOvert

Жыл бұрын

Thanks, I appreciate it!

Thanks man !!

interesting but can we reduce tsp or 0/1 knapsack to sat prblm ? It's so cool though

Is it true that the hardness of the hashing algorithms: SHA-2, SHA-3 relies on the SAT problem?

@NXTangl

10 ай бұрын

Kinda, basically if there exists an algorithm to efficiently invert a hash function or find collisions, the security properties are compromised. So if finding solutions to sha(x) = [known input] or sha(x) = sha(y) is something a SAT-solver can do efficiently, then sha is broken, meaning that if P=NP and we define "can do efficiently" as "can solve in polynomial time," then no hash function is safe (SAT is NP-complete).

At 12:45, why do both x and y must not be the previous value? There could be another satisfiable state with the same x but a different y, so or would make more sense. Looking at the code it does look like the or case. Maybe while saying this you made a mistake 🤔

videoların devamını bekliyorum TÜRKİYEDEN SELAMLAR!!!

Your python sucks, but thanks for the intro!

@HackOvert

Жыл бұрын

Well, we can’t all be masters at everything like you Denis, but thanks for the comment!