Hacker News Reader

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.

View on HN

Thank 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.

This 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

Reply on news.ycombinator.com