3 ms·
Package manager, Static Analysis, Model Checking (like TLA+), probably scheduling software. I'd concur that these are interesting but maybe seldom used pieces
by 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 agoThey 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 agoFor 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 agoYup, TLC is a brute force model checker and Apalache uses SMT.
- hwayne 4y agoMost package managers don't actually use SAT, because it's hard to get data about the version conflicts when it's unsatisfiable.