zero_k

14 ms·

91.
by zero_k 3y ago
I am very tired of this quantum computing nonsense. I have been hearing about it overtaking everything for almost 20 years (when I did my PhD). While the EU and the US has been pumping money into quantum for all these years, they completely
92.
by zero_k 3y ago
This is cool :) My only small gripe is that python-sat (i.e. pysat) is nice, but it kinda hides all the work that SAT solver writers (like me... :D) do. It gives a nice interface to access them all, but it also means that e.g. if something
93.
by zero_k 3y ago
Haha yes, that's the norm. They don't care. Report to the regulator. Then they care. Find out who the regulator is in your country, and report to them. Kinda annoying, but when the regulator tells them they need to do it, it magic
94.
by zero_k 3y ago
Wow, nice, thanks! :heart:
95.
by zero_k 3y ago
Hahahahaha good point!
96.
Probabilistic Approximate DNF volume counting(msoos.org)
2 points by zero_k 3y ago|1 comments
97.
by zero_k 3y ago
A cool method to approximately count volume using the power of randomization. It's a pretty simple algorithm, each step being trivial on its own, yet it produces a surprising good algorithm for a rather complicated problem.
98.
by zero_k 3y ago
That's a cool story! Would have loved to have heard more about that :)
99.
by zero_k 3y ago
I work on a regular basis with the author, and we have discussed caste before. I guess the most I can add to the story is that he is very supportive of all those who have not been given the chance, for whatever reason, to excel. For example
100.
by zero_k 3y ago
Hahha, I am Mate :) I still think that GPGPU can't help in the core of the algorithm. However, I was pleasantly surprised with Nicolas' work. He is a proper magician, and he had a great idea and made it work. Notice that he didn&#
101.
by zero_k 3y ago
For anyone who understands easier through code, I suggest: https://github.com/msoos/minisat-v1.14 It's an early version of MiniSat by Niklas Eén and Niklas Sörensson. You can get the original ZIP from minisat.se,
102.
by zero_k 3y ago
That is true, but there are many interesting heuristics in modern SAT solvers, such as kissat: https://github.com/arminbiere/kissat (winner for a few years now). LBD ("glues" in glucose) is one of them. Kissa
103.
by zero_k 3y ago
There is a solver that can make effective use of GPUs (shameless self-promotion): https://github.com/nicolasprevot/GpuShareSat It is a VERY fun work. Code entirely written by Nicolas Prevot, a magician of CUDA. Paper l
104.
by zero_k 3y ago
No, parallel SAT solvers are NOT disqualified, in fact there is a parallel track. Seriously? Every year there is a winner for the parallel track. Here's last year's: https://satcompetition.github.io/2022/resul
105.
by zero_k 5y ago
The company I know handles account "deletions" by pseudonymizing data, which is utter BS, any half-competent engineer can recover who the original person was. The engineering lead in charge realized he can get promoted by calling
106.
by zero_k 5y ago
People here talking about PII reminds me every day that we still haven't grasped what Personal Data is, and how incredibly different it is from PII. Ah, sad.
107.
by zero_k 6y ago
+1. I am always surprised that they used to do (and of course still must do) proper full-on formal verification of e.g. train track scheduling systems, so train accidents, and consequently 100s of deaths don't just happen because &quot
108.
by zero_k 6y ago
Yes. It turns out that squeezing more performance out _purely_ from the silicon has been mostly due to: (1) hand-rolled memory layouts that optimize placement, do bit-stuffing and the like to take the most advantage of the cache, (2) using
109.
by zero_k 6y ago
Ah, good point. Still, the most used theories are mostly SAT-bound. BV (bitvector) especially. And the translation to SAT can play a huge part, so even in BV logics, the SMT solver's abilities are super-important. But runtime in these
110.
by zero_k 6y ago
Hah, funny to see my blog referenced. Yeah, cache misses are a huge part of SAT solving (modern solvers have prefetch code specifically for this loop, some seemingly following the code I wrote). And SAT solving is about 95+% of SMT solving.
111.
by zero_k 7y ago
Ah, good old days. I wrote some of the tooling back in the days. Was a lot of fun. Damn, video cards have advanced so much in the past years I wonder how fast that code would now run. We were using Radeon 5970s at the time -- integer perfor
112.
by zero_k 7y ago
I like the article, it gets to the point. I would, however, change this: " 3. Hire the best engineers you can." to: "3. Hire and work hard to keep the best managers and engineers you can." As they mention, accumulating k
113.
by zero_k 7y ago
There is a SAT solver (mine, actually :) ) that's also complied to WASM, and online: https://msoos.github.io/cryptominisat_web/
114.
by zero_k 8y ago
(author here) Well, those are all valid strategies. In fact, in the original work that introduced CryptoMiniSat, I used state saving (you called this copying) to quickly reset state to an old one. One could also say that polarity caching is
115.
by zero_k 9y ago
For smaller problems, the fancier solvers are actually worse than MiniSat/Picosat. That's because of the overhead of creating and maintaining datastructures and the fancy preprocessing. The larger, more complex solvers are meant t
116.
by zero_k 9y ago
Improving heuristics... everybody has been doing that, but based on _very_ sparse information, mostly just running times and number of conflicts&decisions. I leads to poor understanding and slow improvement of heuristics. I think we ou
117.
by zero_k 9y ago
Wow, that's kinda interesting. I somehow cannot get rid of the feeling of having a really nice hammer and then treating everything as a nail. There are other uses of deep/machine learning that could help SAT solvers. For example,
118.
by zero_k 9y ago
The whole society is getting short-changed by the idiots trying to make a sacrificial goat out of her/him. Anybody who doesn't understand why s/he doesn't talk, should read Sydney Dekker's books (in particular, &quo
119.
by zero_k 9y ago
That's a joke. It would take them a lot more to fix than 400k. Just the pentests + risk assessments would cost more and they would also need to educate their personnel (developers, testers, DevOps, managers), and implement new policies
120.
by zero_k 9y ago
Sure, he was wrong. So was Newton. Einstein fixed some of it, and then a lot of others fixed some of the remaining parts, etc. Writing "Satoshi was wrong" as a headline, is misleading at best. Why would someone talk about Satoshi

More ›