zero_k

I get you. It took me a looong time to come to terms with the fact that I can buy myself some nice things, even though I was already gifting nice things to others. I still only rarely buy nice stuff for myself, but I am learning. I bought myself a high-end computer (5950x & RTX 3070) 3 years ago, and I realized how important it is to spend -- it's sometimes cheaper than buying it later (it was the beginning of the silicon crisis), and you get to enjoy it a lot. I still pay a lot of attention to what I buy and for what purpose, but I am less crazy about not spending it.

It takes actual time to learn to spend, and you gotta be patient with yourself.

I read that many (10? 15?) years ago and it changed me. It literally, changed me. That blog post, and its comments (including one by the sister of the author... really difficult stuff) is incredibly hard and important to read.

Indeed. If you wanna understand this more in-depth, I suggest the book "Can't Catch a Break: Gender, Jail, Drugs, and the Limits of Personal Responsibility". It does exactly what it says on the lid, an amazing book.

Haha null deref is funny. Not surprised they are so bad still. They were terrible back then. Didn't improve over time.

This confirms what everyone who ever touched AMD GPGPUs knows -- that the only thing holding back AMD from becoming a 2 Trillion dollar company is their absolutely atrocious software. I remember finding a bug in their OpenCL compiler [1], but crashing their OpenCL compiler via segfault was also a piece of cake (that was never fixed, I gave up on reporting it).

AMD not developing a competitor to CUDA was the most short-sighted thing I have ever seen. I have no idea why their board hasn't been sacked and replaced with people who understand that you can make the best hardware out there, but if your SW to use it is -- to be very mild -- atrocious, nobody is gonna buy it or use it.

Us, customers, are left to buy the overpriced NVidia cards because AMD's board is too rich to give a damn about a trillion or so of value left on the table. Just... weird. Whoever owns AMD stock I hope is asking questions, because that board needs to go down the nearest drain.

[1] https://github.com/msoos/amdmiscompile -- they eventually fixed this

The imminent nonsense of fear-mongering and money wasting, mostly. Academic funds spent billions on PQC and academia has been paid to shill nonsense for long enough to convince some of these players to "ah, let's just integrate PQC, whatever". It's nothing more than a waste of money and resources.

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 missed the AI revolution, and have been chronically underfunding basic research (e.g. what I'm partial to, formal methods). You can still get tons of money from funding agencies by _somehow_ incorporating "quantum" into your funding proposal. It's a joke.

I remember being at the SAT conference 2 years ago (co-located with all other formal methods conferences), and I raised my concern about the BS that was accepted as a research paper again doing some nonsense quantum stuff, and the person from Intel was like, we are almost at 100 qbits, end of the year! Pinky Promise! Of course none of that happened. They promised 1000s of qbits in just a decade 20 years ago.

Best part is that even when they have 10s of thousands of qbits they can't show me a single, actually useful, revolutionary application other than breaking RSA, which is laughable (yada-yada some optimization problems, sorry, but no, the more you dig, the more it's obvious it is nonsense). Billions of EUR into this fever dream and they got completely blind-sided by deep learning (which they _also_ under-funded until industry picked it up and made it work). It's the same idiots who demoted Katalin Kario who recently got the Nobel recently for mRNA vaccines. I sometimes really get tired of Academia.

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 doesn't work, the user may not know who to contact as they may not be aware which SAT solver they are using. I guess it's the rule of something becoming so mainstream that the authors of the underlying technology fade away, and those doing the (actually really hard work!) of maintaining the common API are referenced only.

I have seen publications/work where the SAT solver was credited only as pysat, which is not a SAT solver :) Kinda cool and sad at the same time!

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 magically gets done.

Note that the regulator doesn't threaten with childish things like a fine of 1M USD, that's kids' playground stuff. They threaten to revoke their banking license, which will cost them 100x more per day :)

Wow, nice, thanks! :heart:

Hahahahaha good point!

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.

That's a cool story! Would have loved to have heard more about that :)

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 he is a staunch supporter of women's rights (just check out his track record of both hiring and retaining female talent as PhD/PostDoc), and speaks up regularly for those who are oppressed.

I like that he used Freedom of Information regulation to get information on discrimination. This reminds me of an old friend who did the same here in Germany, about West vs East-Germany born heads of universities. The ratio is way-way worse than you might imagine. It's not the same level of oppression as in India, but those who think this issue is far from Europe need not look further than the heart of the EU itself.

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't make the GPU do propagation/conflict generation. Instead, he used it to better distribute clauses between the threads that do all of that. In a way, he improved clause cleaning. When I saw his work, I was very-very happy.

I still hold that GPGPUs can't do CDCL. However, they may be helpful in some of its sub-parts, or may be able to run another algorithm for solving SAT that we haven't invented yet.

Just my 2 cents,

Mate

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, but it's easier to read from GitHub. Enjoy!

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. Kissat is actually quite readable. More readable is CaDiCaL, also extremely fast and effective: https://github.com/arminbiere/cadical

I personally also develop a SAT solver called CryptoMiniSat, but the above two are easier to read :)

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 link here: https://comp.nus.edu.sg/~meel/Papers/sat21-psm.pdf

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/results.html

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 pseudonymization "anonymization" thereby fooling most, and not losing the data for the company. Those who knew he was making a mess were not included in the data deletion project, likely because it was inconvenient to hear the truth.

So that's how a huge company deals with "data deletion". I hope the DPA will come down on them hard but of course this clown will then just go and do this circus at another company, now promoted to high heavens.

I hate that privacy and security are full of snake oil peddlers, and it pays of extremely handsomely to be a snake oil peddler. It's not in anyone's interest for you to get caught (who wants to advertise their security is bad/they don't abide by GDPR?), so even if it becomes painfully obvious you've been selling snake oil, you'll only be asked to hand in your resignation, allowing you to do the same (but at an even higher level) at another company.

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.

+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 "sorry for the bug, ver 1.2 fixes it" -- but people are happy to sit into a Tesla going at 120km/h and allow a well-tested, but not formally verified deep learning system to make decisions. BTW, I know it's not formally verified, because formally verifying deep learning systems is a currently very much unsolved problem for anything but toy examples.

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 clever data structures that cache certain elements of the pointed-to data in the data we read linearly, thereby allowing the cache to pre-fetch them and allow us not to (always) dereference the pointer, (3) prefetching.

Note that (1) and (2) are much more important than (3). In particular, you can even arrange the data elements for (1) in an order that you _expect_ them to be dereferenced, and even if your "hit" ratio is only slightly better than zero, you can get a performance improvement. For this latter one, check out https://www.msoos.org/2016/03/memory-layout-of-clauses-in-mi...

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 logics are dominated by the SAT solver. I should play with more SMT solvers.

I work on the STP SMT solver along with a team of very dedicated people (https://github.com/stp/stp/), it's QF_BV (Quantifier Free BV) solver and it tends to do well in the competitions: https://smt-comp.github.io/2020/results.html So I'm probably a bit biased towards BV. For counting (e.g. https://github.com/meelgroup/approxmc) and sampling (e.g. https://github.com/meelgroup/unigen) it's also 99% SAT solver runtime.

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. So, yeah, cache is where it's at.

I once had an old, but "enthusiast" i7 that had a 3-lane mem setup, and "upgraded" to a consumer dual-lane i7 that was 2-3 gens ahead. It had the same performance(!) for SAT solving. Was pretty eye-opening.

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 performance was pretty bad on NVidia cards back then.

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 knowledge is important. Keeping that knowledge around is therefore also important (and sometimes difficult). The best managers will know what technical debt is, how to handle pressure from higher-ups, and how to keep a team happy, healthy and productive.

There is a SAT solver (mine, actually :) ) that's also complied to WASM, and online:

https://msoos.github.io/cryptominisat_web/

(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 in fact saving redo-information (at least to some extent -- to what extent, can debated). The thing is -- I am not a pro at these other strategies and I can't talk about them with the same clarity. At the end of the day, all of these are quite abstract in some way -- there are many design choices to be made and many different designs.

I just tried to highlight brute force vs. partial evaluation&backtrack. But of course there are many other comparisons to be made. I'm just conscious that I have neither the time nor the expertise to do these all unfortunately :( I let Knuth do the heavy lifting, doing all the comparisons in his books.

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 to have a better chance to solve more complex problems and will use hybrid strategies to make sure they don't accidentally go down into some rabbit hole. So I would expect them to have better consistency.

Note that winning in the competition, until 2017, meant you solved the most instances, each with a ~5000s timeout. So if you solved every single one within 4999s you won, you were the best... This obviously encouraged incredibly long startup times that are gained back over the overall 5000s timeout. It clearly does not mimic normal use-cases.