Solving Reconfiguration Problems of First-Order Expressible Properties of Graph Vertices with Boolean Satisfiability
Takahisa Toda, Takehiro Ito, Jun I. Kawahara, Takehide Soh, Akira K. Suzuki, Junichi Teruyama · 2023
This paper presents a unified framework for capturing a variety of graph reconfiguration problems in terms of firstorder 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.