7 ms·

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 give

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 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!

natpalmer1776 3y ago
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"
klysm 3y ago
And that's exactly the power of SAT right? It's a universal way of expressing a large set of problems.
- everforward 3y ago
  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).
  - Sesse__ 3y ago
    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.)
    - everforward 3y ago
      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.
rapfaria 3y ago
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?
- madars 3y ago
  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.
- lucideer 3y ago
  > But as an user, why would he/she care about how it works 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.
  - yareal 3y ago
    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.
    - lucideer 3y ago

by zero_k 3y ago

natpalmer1776 3y ago

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"

klysm 3y ago

And that's exactly the power of SAT right? It's a universal way of expressing a large set of problems.

everforward 3y ago
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).
- Sesse__ 3y ago
  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.)
  - everforward 3y ago
    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.

rapfaria 3y ago

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?

madars 3y ago
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.
lucideer 3y ago
> But as an user, why would he/she care about how it works 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.
- yareal 3y ago
  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.
  - lucideer 3y ago