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

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 https://en.wikipedia.org/wiki/List_of_model_checking_tools