3 ms·
This is exactly what SAT and SMT are for. SMT is some extra stuff on top of SAT. There are a few frameworks which extend SAT. I'd look at minizinc, it is a fai
by CJefferson 7y ago
This is exactly what SAT and SMT are for.
SMT is some extra stuff on top of SAT. There are a few frameworks which extend SAT. I'd look at minizinc, it is a fairly easy to use language which can produce SAT (and SMT, and others) as output. Often encoding things in SAT directly gets arkward.
- The_rationalist 7y agoThank you but as you say, encoding is limiting. SMT are a progress versus SAT. But I believe I would need an SMT that take a graph and rules as input and verify if the graph or parts of the graph satisfy the rules/constraints. And output me the indexes of the satisfied parts of the graph. I believe such a thing does not yet exist.
- zzz95 7y agoThis is what model checkers are for. They internally (might) use SAT solvers to reason over transition graphs. The general problem for model checkers is of this form: System description: Transition system like automata or a guarded command language which induces a graph. System Property: Stated in some logic, CTL/LTL Output: Satisfied, or Unsatisfied with a counter example (usually a path in the graph which is false). If your problem can fit into such a framework, have a look at model checkers: https://en.wikipedia.org/wiki/List_of_model_checking_tools https://en.wikipedia.org/wiki/List_of_model_checking_tools