Comment by The_rationalist

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.