4 ms·

>> Fast SAT solvers power a lot of the interesting software out there. Can you give examples? I can't think of anything I use regularly that would use that, wi

>> Fast SAT solvers power a lot of the interesting software out there. Can you give examples? I can't think of anything I use regularly that would use that, with possible exceptions of Make and maybe a compiler (for optimisation)

F-W-M 4y ago
Package manager, Static Analysis, Model Checking (like TLA+), probably scheduling software. I'd concur that these are interesting but maybe seldom used pieces of software, except for package management.
- F-W-M 4y ago
  They play a big role in hardware design and verification as well. All in all, SAT solvers became very good, so the solution to many NP-hard problems is to encode them in SAT and solve them this way.
- hcs 4y ago
  For model checking Alloy might be a better example, it directly builds SAT instances (through the Kodkod constraint solver) that are then solved with a SAT solver. I don't think the standard TLA+ checker (TLC) uses SAT explicitly, though there's an alternate checker (Apalache) that uses a Satisfiability Modulo Theories solver like Z3. (Caveat that I've been wrong about stuff like this before, never dug into the implementation of TLA+ tools, but that's what I pick up from https://lamport.azurewebsites.net/tla/tools.html https://lamport.azurewebsites.net/tla/tools.html )
  - hwayne 4y ago
    Yup, TLC is a brute force model checker and Apalache uses SMT.
- hwayne 4y ago
  Most package managers don't actually use SAT, because it's hard to get data about the version conflicts when it's unsatisfiable.
fooker 4y ago
Think of it in terms of weird graph problems and algorithms. It is now easier and faster to encode most graph problems and have a SAT solver go at it, compared to carefully designing and tuning your custom graph algorithm for performance in the kinds of graphs you care about. As for examples, there isn't much retail software that really needs SAT. But you might have indirectly used firewall/configuration management, home automation, flight/factory scheduling, route planning, etc.
Hendrikto 4y ago
Print shops use SAT solvers to lay out pages on a large sheet of paper in the most efficient way, for example.
IshKebab 4y ago
He's stretching the definition of "interesting" I think. The main application of modern SAT solvers (and SMT solvers) is formal verification, which I do think is interesting, but you're very unlikely to be using it. There are some other uses, e.g. for programming languages with advanced type systems, but I doubt most people interact with SAT solvers basically ever.
- fooker 4y ago
  Have you used, interacted with, or benefited from AWS? ;) You are right that most people do not have to interact with SAT solvers. Everyone has, almost surely, interacted with software with uses SAT solvers or have used SAT solvers for development tools. If not software, your chips were definitely designed using tools which are nowadays based on SAT.
  - IshKebab 4y ago
    > If not software, your chips were definitely designed using tools which are nowadays based on SAT. To some degree sure (assuming a generous definition of "designed"). I mentioned formal verification, and I expect synthesis uses it a bit. Still a pretty minor use IMO. You definitely could still design chips without SAT/SMT.

F-W-M 4y ago

Package manager, Static Analysis, Model Checking (like TLA+), probably scheduling software. I'd concur that these are interesting but maybe seldom used pieces of software, except for package management.

F-W-M 4y ago
They play a big role in hardware design and verification as well. All in all, SAT solvers became very good, so the solution to many NP-hard problems is to encode them in SAT and solve them this way.
hcs 4y ago
For model checking Alloy might be a better example, it directly builds SAT instances (through the Kodkod constraint solver) that are then solved with a SAT solver. I don't think the standard TLA+ checker (TLC) uses SAT explicitly, though there's an alternate checker (Apalache) that uses a Satisfiability Modulo Theories solver like Z3. (Caveat that I've been wrong about stuff like this before, never dug into the implementation of TLA+ tools, but that's what I pick up from https://lamport.azurewebsites.net/tla/tools.html https://lamport.azurewebsites.net/tla/tools.html )
- hwayne 4y ago
  Yup, TLC is a brute force model checker and Apalache uses SMT.
hwayne 4y ago
Most package managers don't actually use SAT, because it's hard to get data about the version conflicts when it's unsatisfiable.

fooker 4y ago

Think of it in terms of weird graph problems and algorithms. It is now easier and faster to encode most graph problems and have a SAT solver go at it, compared to carefully designing and tuning your custom graph algorithm for performance in the kinds of graphs you care about. As for examples, there isn't much retail software that really needs SAT. But you might have indirectly used firewall/configuration management, home automation, flight/factory scheduling, route planning, etc.

Hendrikto 4y ago

Print shops use SAT solvers to lay out pages on a large sheet of paper in the most efficient way, for example.

IshKebab 4y ago

He's stretching the definition of "interesting" I think. The main application of modern SAT solvers (and SMT solvers) is formal verification, which I do think is interesting, but you're very unlikely to be using it. There are some other uses, e.g. for programming languages with advanced type systems, but I doubt most people interact with SAT solvers basically ever.

fooker 4y ago
Have you used, interacted with, or benefited from AWS? ;) You are right that most people do not have to interact with SAT solvers. Everyone has, almost surely, interacted with software with uses SAT solvers or have used SAT solvers for development tools. If not software, your chips were definitely designed using tools which are nowadays based on SAT.
- IshKebab 4y ago
  > If not software, your chips were definitely designed using tools which are nowadays based on SAT. To some degree sure (assuming a generous definition of "designed"). I mentioned formal verification, and I expect synthesis uses it a bit. Still a pretty minor use IMO. You definitely could still design chips without SAT/SMT.