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!
But as an user, why would he/she care about how it works on the background, even if there is an issue? Surely the average Factorio player is perhaps familiar with programming, but isn't working over an abstraction exactly why solutions like these work?
I find this (extremely prevalent) perspective increasingly demoralising.
Why wouldn't he/she care?
There's an important distinction here between the use of the word "should" and "would". The user of course shouldn't be required to care, but making a decision on their behalf that they won't is fundamentally different.
This is of course largely driven by the sorry state of UX where the responsibility to integrate rich choice & flexibility into refined simple interfaces is shirked in favour of achieving the same simplicity via the lazier approach of design minimalism.
Who wrote the network transport code that shepherded the bits from your post to the hacker news backend? What Ethernet devices did it transit and who wrote that code? What tradeoffs were made between hardware performance characteristics in the interrupt handlers in your network card? What about your keyboard? Did you choose cat 5 or cat 6 cables for this post to HN? Were those cables shielded?
There are many many occasions where something is below the level of abstraction that you care about. Don't assume that because you care about a particular level of abstraction that everyone else should too.
Are you asking whether I know these things or whether I'd like to? Or whether I'd like the freedom to make choices about these questions -vs- each of them being chosen for me without opportunity for input or insight?
I don't think it's particularly controversial to say that, for most people, independent of their level of technical knowledge, the ideal is for answers to all of your questions to be available & accessible in some way, & for there to be choice in that market.
People can choose to take simple defaults without delving into the hows & whys but I can't see why those same people would object to others having choice & transparency around those defaults.
In summary: I don't know what point you're trying to make.
You asked "why wouldn't they care?" I'd argue you don't care below some level of abstraction.
I'm pointing out that we all have a limited capacity to care at different levels of depth. And people might not want to care because they have other things they want to care about.
You don't care about the whole stack you use. Others don't either, you sound like you are chastising others for not caring.
You sound like you're reading things from my comments that suit your own rebuttal rather than what I've actually said.
From my first comment:
from my second comment;
I'm literally just arguing for choice, transparency & availability. I'm not proposing placing any further burdens on users regardless of what they want to care about.
Anyone can learn these things (the workings of pysat) if they want to. Sometimes the inner workings and history of things is hidden as proprietary secrets, but usually that isn't the case and somebody who's curious can dig into how things work and who invented them.
This is very true in this case, but not in all cases, & I think the gp's point w.r.t. such things being (relatively) obscured applies universally. All systems stand to benefit from constructive feedback on things being clearer & more transparent.
and because this attitude has become so prevalent people now pile shoddy abstraction on top of shoddy abstraction without interest or ability to reason about what that does down the stack.
The lesson from this isn't "you don't need to care about how things work" but invest some time into going one or two levels deeper than you "need" to. If you have no idea how things work under the hood the moment things tend to break or leak you're going to end up clueless.
The question is: where do you draw the line?
* The SAT wrapper? * The SAT library? * The math library the SAT library depends upon? * The LibC? * The operating system? * The processor? * The lithography machine manufacturers? * The guys that provided the raw silicone?
There's no hard line to be drawn anywhere - trying to shoehorn the argument into the metaphor of a line somewhere doesn't track.
Two framings to attempt to answer your question reasonably:
Framing 1: Should information on all the things you listed be available & accessible? In an ideal world, I think so.
Of course that doesn't translate to all of them being pushed into users faces while they attempt to play Factorio (they don't even know how to install python & haven't even unlocked balancers yet). It just means: can I find it on the internet. Right now, thankfully, I can for most of it (sadly silicon supply chain transparency isn't quite where it could be).
Framing 2: Should the above information be readily apparent: that's a question that's much more dependent on degrees of abstraction. In this case, the gp is offering feedback that the SAT libraries are at a level of abstraction that makes them relevant enough to someone running the python tool in their cli. I would tend to agree.
"...or as I've taken to calling it recently, SAT slash LAPACK slash MUSL slash GNU slash Linux"
Techbros always insist on infantilizing users. I think it's a weird combination of gatekeeping and a superiority complex.
Why do you use Techbros as a derogative term here? How does it contribute to the discussion?
Why is it gatekeeping, if you ask for UIs that are not only optimized for the most novice user, but also for more advanced users? I'd say it is the other way around. People designing UIs that can only be used for the most easy tasks are gatekeeping. They are keeping out the power users or those who want to become a power user. I've often wondered whether the lack of a smooth path between tools for laymen and tools for professionals is the true reason why it is hard to use computers for more than content consumption.
I think you might have misinterpreted the commenter you're replying to: it sounds like you're arguing for the same side of the argument?
I don't see this that critically. Joe Schmoe and Programmmer Paul live in two different worlds. Joe might be into finace where I don't care about how anything is calculated so long as the right amount is in my bank account by the end of the month. Maybe they use a fancy excel sheet or SAP-FI or whatever.
I don't think that the missing interest in either topics is particulary demoralizing.
But on a different note: it is demoralizing when you need to cooperate with that other world, when Paul needs to create that program in sap for the calculations and Joe does not care for the inner workings or Paul for the formulas. That makes communication so much harder.
This is essentially the problem: the driving of the world to extremes. Joe's & Paul's worlds are demarcated by the systems they operate in. Their knowledge is not only limited by their primary areas of interest but by what's made evident to them through their daily interactions.
As an individual Paul may have zero interest in "Joe's world" & Joe may individually have less than zero interest in what solvers are operating in Factorio, but those are individual stories, not generalities. When you're generalising about people you're looking at a spectrum of interest within which you need to acknowledge that (a) programmers are humans who use tools too: DX isn't the only area that needs to cater to programmers, they also use Spotify & banking apps & play games just like everyone else. And (b), similarly there's a million Joes out there who will never write a line of code but still possess a technical interest that goes beyond wilful ignorance.
The vast majority of Factorio players are not familiar with programming. A small but very vocal and very enthusiastic minority are though.
At least in the past some SAT solvers were vastly better on certain kinds of problems. E.g. cryptominisat had native handling of XOR clauses which no other solver did. By referencing pertinent details of your experimental setup you could save others who want to build upon your work a lot of time.
And that's exactly the power of SAT right? It's a universal way of expressing a large set of problems.
In the same sense that SQL is a universal way of expressing a large set of problems.
I.e. all the implementations speak the same language, but they operate and prioritize differently.
SAT solvers are NP-Hard, so there isn't a single SAT solver to rule them all. Which one you choose matters, same as with databases. CockroachDB, PostgreSQL and SQLite all speak SQL, but are not interchangeable. Same with SAT solvers.
I'd agree with OP; the SAT writers should get more credit. It's a hard problem, and I'd bet most of us are either incapable or unwilling to spend ages working on it (myself included, no shade intended). It's also vitally important. To my understanding, SAT solvers underly most package managers. It's how npm or pip or apt know what version to install for each package such that no version violates another packages constraints (if any, it's also where the "no valid version combinations exist" message comes from).
apt doesn't use a SAT solver; it has its own heuristics. (Seemingly it _can_ call out to an external one if you give the --solver argument, which in 20+ years of Debian I have never seen anyone use, and which I didn't know of before I made a search now to make sure.)
Oh, that's interesting, thanks for the correction!
Now I have some reading material for when I'm bored. I'm curious how they handle it without a SAT solver.
In a way, you and every other author who created a SAT solver being used by pysat ARE pysat! :)
Another way to look at it is that you are the "giant" in the famous quote "If I have seen further than others, it is by standing on the shoulders of giants"