Solving Reconfiguration Problems of First-Order Expressible Properties of Graph Vertices with Boolean Satisfiability

This paper presents a unified framework for capturing a variety of graph reconfiguration problems in terms of first-order expressible properties and proposes a Boolean encoding for formulas in the first-order logic of graphs based on the exploitation of fundamental properties of graphs. We show that a variety of graph reconfiguration problems captured in our framework can be computed in a unified way by combining our encoding and Boolean satisfiability solver in a bounded model checking approach but allowing us to use quantifiers and predicates on vertices to express reconfiguration properties.