3 ms·

What exactly do SMT systems "solve" in cases like this? If I wrote a simple BFS or DFS and enumerated the search space how far would I get.. Is that not what T

What exactly do SMT systems "solve" in cases like this? If I wrote a simple BFS or DFS and enumerated the search space how far would I get.. Is that not what TLA+ does in principle. I am surprised people prefer having a dependency of something like Z3 at compiler level.

IshKebab 2y ago
They try to find a counter-example to the constraints you have set up, or tell you that no such counter-example exists, in which case your program is correct. The counter-example is in the form of inputs to your program or function. It looks like the TLA+ Proof System does the same thing, but I believe you can also use TLA+ in "brute force all the states" mode. I haven't actually used it.
sunshowers 2y ago
SAT is an NP-complete problem. Doing an exhaustive search is very time-consuming. An SMT or SAT solver uses heuristics to make that process quicker for practical problems. It looks like there are some TLA+ implementations that do use SMT solvers under the hood.
tkz1312 2y ago
SMT solvers use a decision procedure known as CDCL(T). This uses a SAT solver at the core, which operates only on the core propositional structure of the input formula, and dispatches higher level constructs (e.g. functions, arrays, arithmetic) to specialized theory specific solvers. This is an extension of the CDCL (conflict driven clause learning) approach to SAT solving, which is a heuristic approach that uses information discovered about the structure of the problem to reduce the search space as it progresses. At a high level: 1. assign true or false to a random value 2. propagate all implications 3. if a conflict is discovered (i.e. a variable is implied to be both true and false): 1. analyze the implication graph and find the assignments that implied the conflict 2. Add a new constraint with the negation of the assignment that caused the conflict 3. backtrack until before the first assignment involved in the conflict was made The theory specific solvers use a diverse set of decision procedures specialized to their domain. The “Decision Procedures” book is an excellent overview: http://www.decision-procedures.org/ http://www.decision-procedures.org/
oggy 2y ago
TLA+ has also had an SMT-based backend, Apalache [1], for a few years now. In general, you encode your system model (which would be the Rust functions for Verus, the TLA model for Apalache) and your desired properties into an SMT formula, and you let the solver have a go at it. The deal is that the SMT language is quite expressive, which makes such encodings... not easy, but not impossible. And after you're done with it, you can leverage all the existing solvers that people have built. While there is a series of "standard" techniques for encoding particular program languages features into SMT (e.g., handling higher-order functions, which SMT solves don't handle natively), the details of how you encode the model/properties are extremely specific to each formalism, and you need to be very careful to ensure that the encoding is sound. You'd need to go and read the relevant papers to see how this is done. [1]: https://apalache.informal.systems https://apalache.informal.systems

IshKebab 2y ago

They try to find a counter-example to the constraints you have set up, or tell you that no such counter-example exists, in which case your program is correct. The counter-example is in the form of inputs to your program or function. It looks like the TLA+ Proof System does the same thing, but I believe you can also use TLA+ in "brute force all the states" mode. I haven't actually used it.

sunshowers 2y ago

SAT is an NP-complete problem. Doing an exhaustive search is very time-consuming. An SMT or SAT solver uses heuristics to make that process quicker for practical problems. It looks like there are some TLA+ implementations that do use SMT solvers under the hood.

tkz1312 2y ago

SMT solvers use a decision procedure known as CDCL(T). This uses a SAT solver at the core, which operates only on the core propositional structure of the input formula, and dispatches higher level constructs (e.g. functions, arrays, arithmetic) to specialized theory specific solvers. This is an extension of the CDCL (conflict driven clause learning) approach to SAT solving, which is a heuristic approach that uses information discovered about the structure of the problem to reduce the search space as it progresses. At a high level: 1. assign true or false to a random value 2. propagate all implications 3. if a conflict is discovered (i.e. a variable is implied to be both true and false): 1. analyze the implication graph and find the assignments that implied the conflict 2. Add a new constraint with the negation of the assignment that caused the conflict 3. backtrack until before the first assignment involved in the conflict was made The theory specific solvers use a diverse set of decision procedures specialized to their domain. The “Decision Procedures” book is an excellent overview: http://www.decision-procedures.org/ http://www.decision-procedures.org/

oggy 2y ago

TLA+ has also had an SMT-based backend, Apalache [1], for a few years now. In general, you encode your system model (which would be the Rust functions for Verus, the TLA model for Apalache) and your desired properties into an SMT formula, and you let the solver have a go at it. The deal is that the SMT language is quite expressive, which makes such encodings... not easy, but not impossible. And after you're done with it, you can leverage all the existing solvers that people have built. While there is a series of "standard" techniques for encoding particular program languages features into SMT (e.g., handling higher-order functions, which SMT solves don't handle natively), the details of how you encode the model/properties are extremely specific to each formalism, and you need to be very careful to ensure that the encoding is sound. You'd need to go and read the relevant papers to see how this is done. [1]: https://apalache.informal.systems https://apalache.informal.systems