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