ZDD-Based Algorithmic Framework for Solving Shortest Reconfiguration Problems

Extracted source text · arXiv 2207.13959

\documentclass[a4paper]{article}
\usepackage[margin=30mm]{geometry}
\usepackage{graphicx}
\usepackage{complexity}
\usepackage{url}
\usepackage{authblk}

\newcommand{\YES}{\mathsf{yes}}
\newcommand{\NO}{\mathsf{no}}
\newcounter{one}
\setcounter{one}{1}
\newcommand{\one}{{\rm \roman{one}}}
\newcounter{two}
\setcounter{two}{2}
\newcommand{\two}{{\rm \roman{two}}}
\newcounter{three}
\setcounter{three}{3}
\newcommand{\three}{{\rm \roman{three}}}
\newcounter{four}
\setcounter{four}{4}
\newcommand{\four}{{\rm \roman{four}}}
\newcounter{five}
\setcounter{five}{5}
\newcommand{\five}{{\rm \roman{five}}}



\newcommand{\ini}{\mathsf{s}}
\newcommand{\tar}{\mathsf{t}}

\newcommand{\TJ}{\mathsf{TJ}}

\newcommand{\X}{\mathcal{X}}
\newcommand{\Z}{\mathcal{Z}}
\newcommand{\sets}{\mathcal{S}}
\newcommand{\zind}{\mathcal{Z}_{\mathrm{ind}}}
\newcommand{\zsol}{\mathcal{Z}_{\mathrm{sol}}}
\newcommand{\labeln}{\mathsf{label}}
\newcommand{\rootn}{\mathsf{root}}
\newcommand{\child}[1]{\mathsf{child}_{#1}}
\newcommand{\remove}{\mathsf{remove}}
\newcommand{\add}{\mathsf{add}}
\newcommand{\swap}{\mathsf{swap}}

\usepackage[ruled,vlined,linesnumbered]{algorithm2e}
\usepackage{amsmath}
\usepackage{amssymb}

\usepackage{CJKutf8}
\newcommand*{\Ja}[1]{\begin{CJK}{UTF8}{ipxm}#1\end{CJK}}

\usepackage{color}
\newcommand{\kawahara}[1]{{#1}}
\newcommand{\KJ}[2]{#2}
\newcommand{\TT}[2]{#2}

\newcommand{\TI}[2]{#2}

\newcommand{\reconfrule}{\mathcal{R}} 

\begin{document}
\title{ZDD-Based Algorithmic Framework for Solving Shortest Reconfiguration Problems} \author[1]{Takehiro Ito} \author[2]{Jun Kawahara} \author[3]{Yu Nakahata} \author[4]{Takehide Soh} \author[1]{Akira Suzuki} \author[5]{Junichi Teruyama}
\author[6]{Takahisa Toda} \affil[1]{Graduate School of Information Sciences,
Tohoku University, Sendai, Japan}
\affil[2]{Graduate School of Informatics,
Kyoto University, Kyoto, Japan}
\affil[3]{Graduate School of Science and Technology,
Nara Institute of Science and Technology, Ikoma, Japan}
\affil[4]{Information Infrastructure and Digital Transformation Initiatives
Headquarters, Kobe University, Kobe, Japan}
\affil[5]{Graduate School of Information Sciences,
University of Hyogo, Kobe, Japan}
\affil[6]{Graduate School of Informatics and Engineering,
The University of Electro-Communications, Chofu, Japan}
\date{}











\maketitle              
\begin{abstract}
This paper proposes an algorithmic framework for various reconfiguration problems using zero-suppressed binary decision diagrams (ZDDs), a data structure for families of sets.
In general, a reconfiguration problem checks if there is a step-by-step transformation between two given feasible solutions (e.g., independent sets of an input graph) of a fixed search problem such that all intermediate results are also feasible and each step obeys a fixed reconfiguration rule (e.g., adding/removing a single vertex to/from an independent set).
The solution space formed by all feasible solutions can be exponential in the input size, and indeed many reconfiguration problems are known to be \PSPACE-complete.
This paper shows that an algorithm in the proposed framework efficiently conducts the breadth-first search by compressing the solution space using ZDDs, and finds a shortest transformation between two given feasible solutions if exists.
Moreover, the proposed framework provides rich information on the solution space, such as the connectivity of the solution space and all feasible solutions reachable from a specified one.
We demonstrate that the proposed framework can be applied to various reconfiguration problems, and experimentally evaluate their performances. 
\end{abstract}

\section{Introduction}

A combinatorial reconfiguration~\TI{}{\cite{IDHPSUU11,Nishimura18,Heuvel13}} is \TI{the problem}{a family of problems} of finding a
procedure that changes one solution of a combinatorial \TI{optimization}{search}
problem into another solution while \TI{satisfying}{maintaining} the
conditions of the \TI{}{search} problem, and has attracted much attention in
recent years. Taking the change of the switch configuration of a
power distribution network as an example, we can regard a switch
configuration \TI{on the network}{satisfying all the electric conditions} as a solution\TI{, and regard finding
the solution that minimizes the power distribution loss as a
combinatorial optimization problem}{~for a search problem~\cite{InoueTWKYKTMH14}.} 
In a reconfiguration version of \TI{the}{this search} problem, the task is to find \TI{the}{a} changing
procedure from the current switch configuration to \TI{the optimal}{another (more desirable)}
one while \TI{satisfying}{maintaining} required \TI{}{electric} conditions such as not causing
power outages. We can say, in general, that a combinatorial
reconfiguration problem models a situation in which we change the current
configuration into \TI{the other}{another} one without allowing the system to stop.

Combinatorial reconfiguration problems have been actively studied
in the theoretical algorithms community in recent years\TI{~\cite{Nishimura18}.}{. (See surveys~\cite{Nishimura18,Heuvel13}.)} In
particular, combinatorial reconfiguration problems related to
graphs, such as independent sets and graph coloring, have been
\TI{well studied}{studied well}. Many of these studies are mainly from a theoretical
perspective, such as analysis of the computational complexity of
the problem \TI{depending on the properties of classes of the input graph, and}{with respect to graph classes;} 
there is little research on the applied aspects to the
best of the authors' knowledge.  
Since many reconfiguration
problems\TI{}{,} such as the independent set reconfiguration\TI{}{~\cite{KaminskiMM12}} and graph 4-coloring reconfiguration\TI{}{~\cite{BC09},} are \PSPACE-complete\TI{~\cite{BC09}}{}, it is hard to design an efficient algorithm. 
However, depending on
applications, the number of vertices in the input graph may be at
most tens or hundreds, and in such cases, we can expect the existence of an algorithm that works in an acceptable time.

There are various promising methods for solving combinatorial
optimization problems that appear in real applications, such as
integer programming, SAT solvers, genetic algorithms,
and metaheuristics. One approach that has attracted attention is the
use of zero-suppressed binary decision diagrams (ZDDs)~\cite{Minato1993,Castro2022}. A ZDD is
a data structure that compresses and compactly represents a
family of sets. By representing the solution set of a
combinatorial optimization problem as a ZDD and by performing set
operations of ZDDs, it is possible to find the optimal solution
by imposing constraints that integer programming methods and SAT
solvers are not good at treating.

In this study, we consider solving combinatorial reconfiguration problems using ZDDs. 
We use the fact that a ZDD not only preserves one\TI{optimal}{} solution, but also \TI{all feasible}{\emph{all}} solutions. 
We propose an algorithm to obtain all solutions that are changeable from a given solution as a ZDD. 
\TI{Our}{This} algorithm can be applied to various combinatorial reconfiguration problems whose solution sets can be represented as ZDDs. 
\TI{We can also impose constraints that can be imposed on the solution set represented as ZDDs, such as the size of the solution. 
Our algorithm can solve the token jumping, token sliding, and token addition and removal models of the independent set reconfiguration problem (their definitions are introduced in the next section). 
\TI{Out}{Our} an algorithm can also handle reconfiguration not only for independent sets, but also for a variety of objects, such as dominating sets, vertex covers, spanning trees, and matchings, where we call them \emph{reconfiguration objects} (or simply \emph{objects}). Our algorithm can be used not only to analyze the changeability between two given solutions, but also to analyze the solution space, such as finding the shortest reconfiguration sequence, finding the solution with the longest shortest sequence from a given solution, deciding the connectivity of the solution space, and finding the optimal solution among solutions changeable from a given solution. What the proposed framework can treat is shown in Fig.~\ref{fig:problems}.}{Although we will give definitions in Section~\ref{sec:preliminaries}, \figurename~\ref{fig:problems} shows combinatorial reconfiguration problems that our algorithm can treat, 
where a combinatorial reconfiguration problem can be identified by the combination of problem variants, change rules (models), and solutions (reconfiguration objects). 
}
We demonstrate the effectiveness of the proposed algorithm by computer experiments.

\begin{figure}[t]
    \begin{center}
    \includegraphics[width=0.9\textwidth]{problems.pdf}
    \end{center}
    \vspace{-2em}
    \caption{Variants, models, and reconfiguration \TI{problems}{objects} that our framework can treat.}
    \label{fig:problems}
\end{figure}

The organization of the paper is as follows.
Section~\ref{sec:preliminaries} defines combinatorial reconfiguration problems and introduces ZDDs.
We propose an algorithm using ZDDs in Section~\ref{sec:framework}.
Section~\ref{sec:versatility} shows that the proposed algorithm can solve various combinatorial reconfiguration problems.
We conduct computer experiments in Section~\ref{sec:experiments} and conclude the paper in Section~\ref{sec:conclusion}.

\if 0
A Zero-suppressed Decision Diagram (ZDD, for short) is a well-studied data structure for efficiently representing a family of sets.
For example, a grid graph of size $8 \times 250$ has $3.07 \times 10^{361}$ independent sets, and a ZDD can represent the family of all the independent sets with only about 1MB memory usage. 
Several efficient algorithms have been developed for constructing a ZDD which represents the family of all feasible solutions for a given problem instance, such as independent sets~\cite{}, xxx~\cite{}, yyy~\cite{}, and zzz~\cite{}. 

In this paper, we utilize ZDDs to solve reconfiguration problems~\cite{IDHPSUU11}, which have been intensively studied in the field of theoretical computer science.
(See surveys~\cite{Nis18,Heu13}.)
In general, reconfiguration problems study the reachability and/or connectivity of solution spaces, defined as follows: 
formed by all feasible solutions. 
There are several variants to be considered, 

Fix a combinatorial search problem and an adjacency relation defined on the feasible solutions for the 

\fi

\if0
We begin with the token jumping model of the independent set
reconfiguration problem.
Hayase et al.\ proposed an algorithm that constructs a ZDD
representing the family of all the independent sets
of a given graph, where the universal set $U$ is the vertex set of the graph. We denote the ZDD by $\zsol$ (we write ``sol'' because of the later generalization).
$\zsol$ is highly compressed if a given graph
has a good structure such as one with small pathwidth.

Our research question is as follows:
Given a graph,
when we have all the independent sets of the graph as a ZDD,
can we use it to solve the reconfiguration problem?
In this paper, we will give a positive solution.
A main obstruction for adapting ZDDs to the reconfiguration
problem is to reconfigure all the elements in a family
represented by a ZDD.
Of course, if we explicitly extract the elements from
a ZDD one by one, it is easy to reconfigure them.
However, to get a benefit of compactness of ZDDs,
we need to construct a ZDD for all the elements
obtained by adapting one step of the reconfiguration
to them without explicitly extracting elements from ZDDs.
For the token jumping model of the independent set
reconfiguration problem, given a ZDD $\Z$ representing
the family of independent sets,
what we need is to construct the ZDD representing
$\{ I \cup \{v\} \setminus \{v'\}
\mid I \in \mathcal{S}(\Z), v \in V \setminus I, v' \in I \}$.
Although a member of them might not be an independent set,
we can restrict only the independent sets by taking
the intersection of $\zsol$ as a ZDD operation.
\fi

\if0

Given a graph $G$ and two independent sets $S, T$ of $G$,
the independent set reconfiguration problem asks us to determine whether there exists a reconfiguration sequence
from $S$ to $T$ or not~\cite{Ito2011}.
A reconfiguration sequence from $S$ to $T$ is a sequence of independent sets
starting with $S$ and ending in $T$ such that for every two consecutive sets $U$ and $U'$ in the sequence,
$U'$ is obtained by removing one arbitrary vertex from $U$
and by adding one arbitrary vertex to the set.
An example is shown in \figurename~\ref{fig:example}.
In general, a combinatorial reconfiguration problem consists of a set of feasible solutions and a set of reconfiguration rules.
The problem is to determine whether there exists a reconfiguration sequence from one feasible solution to the other
such that for every two consecutive solutions in the sequence, the latter solution is obtained by
applying the rules to the former solution.
In this paper, we propose an algorithm for the independent set reconfiguration problem
using zero-suppressed binary decision diagrams (ZDDs)~\cite{Minato1993},
which is a data structure for efficiently representing a family of sets.
This algorithm can be generalized to various reconfiguration problems.

\begin{figure}[t]
    \begin{center}
    \includegraphics[width=0.65\textwidth]{example.pdf}
    \end{center}
    \caption{A sequence $\langle I_{\ini} = I_0, I_1, \ldots, I_5 = I_{\tar} \rangle$ of independent sets of the same graph, where the vertices in independent sets are depicted by large black circles (tokens).}
    \label{fig:example}
\end{figure}

\fi

\if 0

\subsubsection{Problems of the vertex subset type}

(maximal) independent set \cite{IDHPSUU11, DBLP:journals/tcs/KaminskiMM12}, 
(maximal) distance-r independent set, 
(minimal) dominating set \cite{DBLP:journals/jco/SuzukiMN16}, 
(minimal) distance-r dominating set, 
(minimal) vertex cover \cite{IDHPSUU11, DBLP:journals/algorithms/MouawadNRS18}, 
(maximal) clique \cite{IDHPSUU11},
(minimal) k-path vertex cover \cite{DBLP:journals/ieicetd/HoangSY22}, 
(minimal) feedback vertex set \cite{DBLP:journals/algorithmica/MouawadN0SS17, DBLP:conf/iwpec/MouawadNRW14},
(minimal) odd cycle transversal \cite{DBLP:journals/algorithmica/MouawadN0SS17, DBLP:conf/iwpec/MouawadNRW14},

\subsubsection{Problems of the edge subset type}

(Hamiltonian) path \cite{DBLP:journals/tcs/HanakaIMMNSSV20, DBLP:conf/stacs/BousquetI0MOSW22}, 
(Hamiltonian) cycle \cite{DBLP:journals/tcs/HanakaIMMNSSV20, DBLP:journals/algorithms/Takaoka18}, 
(rooted) (spanning) forest \cite{DBLP:journals/algorithmica/MouawadN0SS17}, 
(spanning) tree \cite{IDHPSUU11, DBLP:conf/stacs/BousquetI0MOSW22}, 
spider, 
rainbow spanning tree, 
star \cite{DBLP:journals/tcs/HanakaIMMNSSV20},
non-crossing spanning tree \cite{DBLP:journals/corr/abs-2206-03879}, 
Steiner tree \cite{DBLP:journals/ieicet/MizutaIZ17}, 
caterpillar, 
lobster, 
connected graph \cite{DBLP:journals/tcs/HanakaIMMNSSV20},
(complete) matching \cite{IDHPSUU11}, 
b-matching bipartite \cite{DBLP:conf/mfcs/Muhlenthaler15, DBLP:journals/jco/ItoKKKO19}, 
(i, j)-biclique \cite{DBLP:journals/tcs/HanakaIMMNSSV20}, 
(k-)regular \cite{DBLP:conf/mfcs/Muhlenthaler15, DBLP:conf/walcom/EtoIKOW22}, 
degree-constrained \cite{DBLP:conf/mfcs/Muhlenthaler15, DBLP:conf/stacs/BousquetI0MOSW22}, 
chordal, 
chordal bipartite, 
interval, 
proper interval, 
split, 
(d-)claw-free, 
cograph, 
block, 
threshold, 
gridline, 
trivially perfect, 
strictly clique irreducible, 
bipartite permutation, 
even/odd-hole-free, 
cactus, 
planar, 
outer planar, 
series parallel

\subsubsection{Other reconfiguration problems}

subset sum \cite{DBLP:journals/jco/ItoD14}, 
power supply \cite{IDHPSUU11}, 
set cover \cite{IDHPSUU11}, 
(minimal) hitting set \cite{DBLP:journals/algorithmica/MouawadN0SS17}, 
token sliding on a digraph \cite{arxiv.2203.13435}, 
ball sort puzzle \cite{DBLP:conf/fun/ItoKMOSSUUYY22}

\fi

\section{Preliminaries}\label{sec:preliminaries}

Throughout this paper, we use the symbols $G$, $V$, and $E$ to represent an input graph, its vertex set, and its edge set, respectively.
For families $\mathcal{A}$, $\mathcal{B}$ of sets,
we define $\mathcal{A} \Join \mathcal{B} =
\{A \cup B \mid A \in \mathcal{A}, B \in \mathcal{B} \}$.
In this paper, we sometimes simply call a family of sets a ``family.''

\subsection{Reconfiguration problems}\label{sec:reconf_problem}
\TI{}{As shown in \figurename~\ref{fig:problems}, a combinatorial reconfiguration problem can be identified by the combination of problem variants, models, and reconfiguration objects.

We first define reconfiguration objects.}
Throughout this paper, we use the symbol $U$ to represent a finite universal set, and assume that the \TI{objects for reconfiguration}{solutions for change} can be represented as subsets of $U$. 
More specifically, \KJ{given a reconfiguration problem,} we fix a property $\pi$ defined on the subsets of $U$, and say that a set $X \subseteq U$ is \TI{\emph{feasible}}{a \emph{reconfiguration object} or simply an \emph{object}} if $X$ satisfies $\pi$.

We \TI{also fix a}{then define models, also known as reconfiguration rules. A} \emph{reconfiguration rule} $\reconfrule$ on the subsets of $U$\TI{, which}{} defines whether two subsets of $U$ are \emph{adjacent} or not. 
\TI{}{There are three reconfiguration rules (called Token Addition and Removal, Token Jumping, and Token Sliding models) that have been studied well~\cite{KaminskiMM12,Nishimura18}, where we imagine that a \emph{token} is placed on each element in a subset of $U$. 
\smallskip

\noindent
\textbf{Token Addition and Removal:}
Two subsets $X$ and $Y$ of $U$ are adjacent under the \emph{token addition and removal} (TAR) model if and only if $|(X \setminus Y) \cup (Y \setminus X)| = 1$.
In other words, $Y$ can be obtained from $X$ by either adding a single element in $U \setminus X$ or removing a single element in $X$. 
\smallskip

\noindent
\textbf{Token Jumping:}
Two subsets $X$ and $Y$ of $U$ are adjacent under the \emph{token jumping} model if and only if $|X \setminus Y| = |Y \setminus X| = 1$.
Namely, $Y$ can be obtained from $X$ by exchanging a single element in $X$ with an element in $U \setminus X$. 
\smallskip

\noindent
\textbf{Token Sliding:}
This model is defined only on \KJ{graphs}{an input graph} $G = (V,E)$.
First, consider the case where $U = V$. 
Then, two subsets $X$ and $Y$ of $V$ are adjacent under the \emph{token sliding} model if and only if $X \setminus Y = \{u\}$, $Y \setminus X = \{v\}$, and $\{u, v\} \in E$.
Namely, $Y$ can be obtained from $X$ by exchanging a single vertex $u \in X$ with its \KJ{neighbor} adjacent vertex $v \in V \setminus X$. 
Next, consider the case where $U = E$. 
Then, two subsets $X$ and $Y$ of $E$ are adjacent under the \emph{token sliding} model if and only if $X \setminus Y = \{e\}$, $Y \setminus X = \{e'\}$ and $e$ and $e'$ share one of their endpoints. 
Namely, $Y$ can be obtained from $X$ by exchanging a single edge $e \in X$ with its incident edge $e' \in E \setminus X$. 
\smallskip

We finally define problem variants.
For} a given universal set $U$, the \emph{solution space} under the property $\pi$ and the reconfiguration rule $\reconfrule$ is a graph where each node corresponds to a reconfiguration object of $U$, and two nodes are joined by an edge if and only if their corresponding sets are adjacent under $\reconfrule$. 
Then, we can consider various variants of reconfiguration problems on the solution space: 
the \emph{reachability variant} asks whether the solution space contains a path connecting two given objects; 
the \emph{shortest variant} asks to compute the shortest length (i.e., the minimum number of edges) of any path in the solution space that connects two given objects;
the \emph{farthest variant} asks to find an object farthest from a given object in the solution space (i.e., the shortest path between the two objects is the longest);
the \emph{connectivity variant} asks whether the solution space is connected or not;
and the \emph{optimization variant} asks to find an object that is ``optimal'' (e.g., the cardinality of the object is maximum) among objects reachable from a given object. 

\if0
For example, in the independent set reconfiguration problem, we are given two independent sets of the same graph $G=(V,E)$.
There are the following three well-known reconfiguration rules.
Imagine that a token is placed at each vertex of an independent set of $G$.

\noindent
\textbf{Token Jumping:}
For the token jumping model of the independent set reconfiguration problem, each step involves moving a token to any unoccupied vertex.
In other words, two independent sets $S, T \subseteq V$ are adjacent if $|S \setminus T| = |T \setminus S| = 1$.

\noindent
\textbf{Token Sliding:}
For the token sliding model of the independent set reconfiguration problem, each step involves moving a token on some vertex to one of its unoccupied neighbors.
In other words, two independent sets $S, T \subseteq V$ are adjacent if $|S \setminus T| = \{ u \}$, $|T \setminus S| = \{ v \}$ and $\{ u,v \} \in E$.

\noindent
\textbf{Token Addition and Removal (TAR):}
For the token addition and removal (TAR) model of the independent set reconfiguration problem, each step involves either adding or removing a single token such that the resulting independent set is of size at least a given positive integer.
In other words, two independent sets $S, T \subseteq V$ are adjacent if the size of the symmetric difference between $S$ and $T$ is exactly one.


Consider a search problem $\mathcal{S}$ (a polynomial-time
algorithm which, on instance $I$ and candidate solution $y$ of
length polynomial in that of $I$, determines whether $y$ is a feasible
solution of $I$); and fix a polynomially-testable symmetric {\em
adjacency relation} $A$ on the set of feasible solutions, that is, a
polynomial-time algorithm such that, given an instance $I$ of $\mathcal{S}$ and two
feasible solutions $y^\prime$ and $y^{\prime \prime}$ of $I$, it determines whether $y^{\prime}$ and $y^{\prime \prime}$ are
adjacent.  
(In almost all problems discussed in this paper, the feasible
solutions can be considered as sets of elements, and two solutions
are adjacent if their symmetric difference has size 1.)
The {\sc reconfiguration problem for $\mathcal{S}$ and $A$} is the following
computational problem: Given instance $I$ of $\mathcal{S}$ and two feasible solutions
$y_\ini$ and $y_\tar$ of $I$, is there a sequence of feasible solutions
$y_\ini, y_1, \ldots, y_\tar$ of $I$ such that $y_{i-1}$ and $y_i$ are adjacent for $i=1, 2, \ldots, \tar$?
\fi



\subsection{Zero-suppressed decision diagram (ZDD)}\label{sec:zdd}

A ZDD is a data structure for efficiently representing a family of sets.
The definition of a ZDD is given below.
In this section, we set $U = \{x_1, \ldots,x_n\}$
and $x_1 < x_2 < \cdots < x_n$.
A ZDD is a directed acyclic graph (DAG) $\Z$ that has the following properties:
$\Z$ has at most two nodes with outdegree zero, which are called \emph{terminals} and denoted by $\bot$ and $\top$.
Nodes other than the terminals are called non-terminal nodes.
A non-terminal node $\nu$ has an element in $U$, which is called a \emph{label} and
denoted by $\labeln(\nu)$,
and has two arcs, called \emph{0-arc} and \emph{1-arc}.
If the 0-arc and 1-arc of a non-terminal node $\nu$ point at nodes $\nu_0, \nu_1$,
we write $\nu = (\labeln(\nu), \nu_0, \nu_1)$, and we call $\nu_0$ and $\nu_1$ \emph{0-child}
and \emph{1-child}, respectively. Then, $\labeln(\nu) < \labeln(\nu_0)$
and $\labeln(\nu) < \labeln(\nu_1)$ must hold,
where we promise that $x_i < \labeln(\bot)$ and $x_i < \labeln(\top)$
for all $i = 1,\ldots,n$.
The ZDD $\Z$ has exactly one node with indegree zero, called the \emph{root}, and denoted by
$\rootn(\Z)$.

A ZDD $\Z$ represents a family of sets whose universal set is $U$ as follows.
We associate each node in $\Z$ with a family,
denoted by $\mathcal{S}(\nu)$, in the following recursive manner.
The terminal nodes $\bot$ and $\top$ are associated with
$\emptyset$ and $\{\emptyset\}$, respectively;
that is, $\mathcal{S}(\bot) = \emptyset$ and $\mathcal{S}(\top) = \{\emptyset\}$.
Consider the case where $\nu$ is a non-terminal node.
Let $\nu = (x, \nu_0, \nu_1)$, where $x \in U$ and $\nu_0, \nu_1$ are nodes of $\Z$.
The node $\nu$ is associated with the union of the family with which we associate $\nu_0$,
and the family obtained by adding $x$ to each set in
the family with which we associate $\nu_1$;
that is, $\mathcal{S}(\nu) = \mathcal{S}(\nu_0)
\cup (\{\{x\}\} \Join \mathcal{S}(\nu_1))$.
(Note that $\{\{x\}\} \Join \mathcal{S}(\nu_1)$ is the family obtained by adding $x$ to each set in $\mathcal{S}(\nu_1)$.)
Observe that each of the sets in $\mathcal{S}(\nu_0)$ and $\mathcal{S}(\nu_1)$
does not contain $x$ because of the property of ZDDs
i.e., $\labeln(\nu) < \labeln(\nu_0)$
and $\labeln(\nu) < \labeln(\nu_1)$ must hold.
We interpret that the ZDD $\Z$ represents the family with which we associate
the root node.
The family $\mathcal{S}(\Z)$ represented by the ZDD $\Z$
is defined by $\mathcal{S}(\Z) = \mathcal{S}(\rootn(\Z))$
(we use the same notation $\mathcal{S}$ for a node and a ZDD).

Every ZDD $\Z$ has the following recursive structure~\cite{Bryant1986,Minato1993}.
Let $\nu = \rootn(\Z)$ and suppose that $\nu$ is represented by
$\nu = (x, \nu_0, \nu_1)$. Then, for $i = 0, 1$, the DAG consisting of the nodes and arcs
reachable from $\nu_i$ can be considered as a ZDD whose root is $\nu_i$, which we denote $\child{i}(\Z)$.
The ZDD $\child{i}(\Z)$ represents $\mathcal{S}(\nu_i)$.
To compute problems using a ZDD $\Z$, we often design a recursive algorithm $\mathsf{op}(\Z)$, which calls $\mathsf{op}(\child{0}(\Z))$ and $\mathsf{op}(\child{1}(\Z))$ and manipulates the results of them.
To make this clearer, we describe the behavior of the recursive algorithm for the set union operation, using \figurename~\ref{fig:zdd}.
Let us consider to construct the ZDD
 $\mathcal{Z}$ for the union of $\mathcal{S}=\{\{x_1\}, \{x_2\},\{x_1,x_2\}\}$ and $\mathcal{S}'=\{\{x_1,x_3\},\{x_2,x_3\}\}$ from the ZDDs of $S$ and $S'$.
At first, we focus on sets in $\mathcal{S}$ and $\mathcal{S}'$ that do not include $x_1$ and take union over them.
We do this by applying union operation for the left children of the ZDDs for $\mathcal{S}$ and for $\mathcal{S}'$.
The operation is done in a recursive manner: the base step is when one of ZDDs is $\top$ or $\bot$, which is straightforward and omitted.
The induction step is about to be described below.
The same applies to the union for the other sets, that is, the sets in $\mathcal{S}$ and $\mathcal{S}'$ that include $x_1$.
Here we have the two ZDDs as a result of applying recursive operation: one represents all sets in $\mathcal{S}\cup\mathcal{S}'$ that do not include $x_1$ and the other represents those in $\mathcal{S}'$ that include $x_1$, which correspond to $\mathcal{Z}_0$ and $\mathcal{Z}_1$ in \figurename~\ref{fig:zdd}, respectively.
We thus construct the final ZDD $\mathcal{Z}$ so that the $0$-arc of $x_1$ points to $\mathcal{Z}_0$ and the $1$-arc points to $\mathcal{Z}_1$.

Rich operations for manipulating families are provided for ZDDs~\cite{Bryant1986,Minato1993}.
For example, given two ZDDs $\Z, \Z'$, we can efficiently compute ZDDs representing
$\mathcal{S}(\Z) \cup \mathcal{S}(\Z')$, $\mathcal{S}(\Z) \cap \mathcal{S}(\Z')$,
$\mathcal{S}(\Z) \setminus \mathcal{S}(\Z')$, and so on,
using recursive ways described above.
For a binary operation $\circ \in \{ \cup, \cap, \setminus,\ldots\}$,
we denote the ZDD representing $\mathcal{S}(\Z) \circ \mathcal{S}(\Z')$
by $\Z \circ \Z'$.
For more information on ZDDs, please refer to \cite{knuth:taocp41}.

\begin{figure}[t]
  \centering
  \includegraphics[width=\textwidth]{zdd.pdf}
  \caption{Example of a ZDD, the recursive structure, and the removal operation. The second argument of $\remove$ is omitted in the figure. Let $\Z'$ and $\Z''$ be $\child{0}(\Z)$ and $\child{1}(\Z)$, respectively. }
  \label{fig:zdd}
\end{figure}

\section{ZDD-Based algorithmic framework}\label{sec:framework}

\subsection{Algorithmic framework}\label{sec:framework_overview}

We begin with the reachability variant under the TAR model for independent sets, where reconfiguration objects are independent sets in an input graph $G$ of cardinality at least a given threshold $k$.
Hayase et al.~\cite{Hayase1995} proposed an algorithm that constructs a ZDD, say $\zind$,
representing the family of all the independent sets
of a given graph, where the universal set $U$ is the vertex set of the graph and the elements (vertices) in $U$ are ordered.
The ZDD $\zind$ is highly compressed if a given graph
has a good structure, such as one with small pathwidth.
For example, an $8 \times 250$ grid graph has
$3.07 \times 10^{361}$ independent sets, but the ZDD representing them
has just $49{,}989$ nodes (with about 1MB memory usage).

We consider utilizing a ZDD that represents a vast number of independent sets for the reconfiguration problem.
Although $\zind$ includes all the independent sets,
it does not have information on the adjacency relations of independent sets.
What we would like to obtain is the family of independent sets adjacent to a given independent set
and more generally, the family of independent sets
adjacent to any of the independent sets in a given family.
If we can obtain them, by repeating the operation of obtaining the family of adjacent independent sets from the initial independent set,
we can obtain all the independent sets reachable from the initial independent set and decide whether a reconfiguration sequence from the initial independent set to the target one exists.

The TAR model requires two operations: removing a vertex from an independent set and adding a vertex to an independent set.
First, we consider the removal operation.
Given the family $\mathcal{I}$ of independent sets, the removal operation is to remove each element from each independent set in $\mathcal{I}$,
i.e., to obtain the family $\{ I \setminus \{ v\} \mid I \in \mathcal{I}, v \in I \}$.
Given $\mathcal{I}$ as a ZDD,
we propose an algorithm that constructs
a ZDD representing $\{ I \setminus \{ v\} \mid I \in \mathcal{I}, v \in I \}$ without extracting elements from the ZDD.
As the addition operation,
we also propose an algorithm that constructs
a ZDD representing $\{ I \cup \{ v\} \mid I \in \mathcal{I}, v \in U \setminus I \}$.

For later use, we present the two operations in a bit general form.
For a ZDD $\Z$ (whose universal set is $U$) and a set $R \subseteq U$,
let $\remove(\Z, R)$ be the ZDD representing
\[
    \{ I \setminus \{ v\}
        \mid I \in \mathcal{S}(\Z), v \in I \cap R \},
\]
which means that we remove an element only in $R$.
For a ZDD $\Z$ and a set $A \subseteq U$,
let $\add(\Z, A)$ be the ZDD representing
\[
    \{ I \cup \{x\} \mid I \in \mathcal{S}(\Z), x \in A \setminus I \},
\]
which means that we add an element only in $A$.

We can solve the reachability variant of the TAR model of the independent set reconfiguration problem using $\remove(\Z, R)$ and $\add(\Z, A)$ as follows.
First, we construct a ZDD representing the solution space.
Recall that a feasible independent set in the TAR model contains at least $k$ vertices.
It is easy to construct the ZDD, say $\mathcal{Z}_{\ge k}$, representing the family of all the sets with cardinality at least $k$ (i.e., $\{ I \subseteq U \mid |I| \ge k \}$)~\cite{knuth:taocp41}.
The solution space ZDD $\zsol$ is obtained by the intersection operation of $\zind$ and $\mathcal{Z}_{\ge k}$  mentioned in Sec.~\ref{sec:zdd}.

Next, for $i = 0,1,\ldots$,
let $\Z^i$ denote the ZDD representing the family of
independent sets obtained by applying
the reconfiguration rule (i.e., removing or adding a vertex) to $S$ exactly $i$ times,
where $\Z^0$ is the ZDD such that $\sets(\Z^0) = \{S\}$.
The construction of $\Z^0$ is trivial.
For $i = 1,2,\ldots$,
the ZDD $\Z^i$ can be constructed by
\begin{equation}\label{eq:z_i}
    \Z^i \gets  \mathsf{op}(\Z^{i-1}) \cap \zsol,
    \end{equation}
where $\mathsf{op}(\Z) =  \remove(\Z, V) \cup \add(\Z, V)$ for ZDD $\Z$.
Note that $\cup$ and $\cap$ are ZDD operations mentioned in Sec.~\ref{sec:zdd}.
After we construct $\Z^i$, we decide whether $\Z^i = \bot$ (i.e., $\mathcal{S}(\Z^i) = \emptyset$) and whether $T \in \mathcal{S}(\Z^i)$
(both are straightforward tasks).
If $\Z^i = \bot$, it means that the reconfiguration sequence from $S$ to $T$ does not exist because $\mathcal{S}(\Z^j)$, $0 \le j \le i$, includes \emph{all} the independent sets that are reachable from $S$ within $j$ steps.
We output NO and halt.
If $T \in \mathcal{S}(\Z^i)$, the reconfiguration sequence with length $i$ from $S$ to $T$ exists.
We output YES and halt.
If both do not hold, we next construct $\Z^{i+1}$.

\subsection{Removal and addition operations}

Given a ZDD $\Z$ and two sets $A$ and $R$,
we describe how to construct the ZDDs $\remove(\Z, R)$
and $\add(\Z, A)$.

We design an algorithm for $\remove(\Z, R)$ for a ZDD $\Z$, based on the recursive way described in Sec.~\ref{sec:zdd}. 
Let $\nu = \rootn(\Z)$. Suppose that $\nu$ is a non-terminal node and $\nu = (x, \nu_0, \nu_1)$, where $x \in U$ and $\nu_i$ is the $i$-child of $\nu$.

We consider the case of $x \in R$.
Let $\Z^{\mathrm{rem}} = \remove(\Z, R)$ and let us observe characteristics of $\Z^{\mathrm{rem}}$.
First, $\rootn(\Z^{\mathrm{rem}}) = x$ because $\sets(\Z^{\mathrm{rem}})$ contains a set including $x$ and does not contain any set including an element smaller than $x$.
Secondly, let us consider $\child{0}(\Z^{\mathrm{rem}})$,
which is the ZDD representing the family of sets in $\sets(\Z^{\mathrm{rem}})$ not containing $x$.
Each set in $\sets(\child{0}(\Z^{\mathrm{rem}}))$ is obtained by
either of the following two:
(i) we remove an element from a set in $\sets(\Z)$
not including $x$
(i.e., a set in $\sets(\child{0}(\Z))$), and
(ii) we remove $x$ from a set in $\sets(\Z)$ including $x$
(i.e., a set in $\{\{x\}\} \Join \sets(\child{1}(\Z))$).
We collect all the sets of (i) and construct the ZDD representing them.
The ZDD is obtained by recursively applying the $\remove$ operation to $\child{0}(\Z)$.
The ZDD for (ii) is just $\child{1}(\Z)$. Therefore, we obtain
\[
    \child{0}(\Z^{\mathrm{rem}}) = \remove(\child{0}(\Z), R \setminus \{x\}) \cup \child{1}(\Z),
\]
where `$\cup$' is the union operation of ZDDs described in Sec.~\ref{sec:zdd}.

Thirdly, we consider $\child{1}(\Z^{\mathrm{rem}})$,
which is the ZDD representing the family of sets
each of which is obtained by removing $x$
from a set in $\sets(\Z^{\mathrm{rem}})$ containing $x$.
Each set in $\sets(\child{1}(\Z^{\mathrm{rem}}))$ is obtained by
removing $x$ from a set in $\sets(\Z^{\mathrm{rem}})$ containing $x$.
The ZDD is obtained by applying the $\remove$ operation to $\child{1}(\Z)$. Therefore, we have
\[
    \child{1}(\Z^{\mathrm{rem}}) = \remove(\child{1}(\Z), R \setminus \{x\}).
\]

We consider the case of $x \notin R$, which means that we do not remove $x$ from any independent set.
Then, we obtain
\begin{align*}
    \child{0}(\Z^{\mathrm{rem}}) = \remove(\child{0}(\Z), R \setminus \{x\}),\\
    \child{1}(\Z^{\mathrm{rem}}) = \remove(\child{1}(\Z), R \setminus \{x\}).
\end{align*}

Our recursive algorithm for $\remove(\Z, U)$ is as follows:
If $\Z = \bot$ or $\Z = \top$, we just return $\bot$.
Otherwise, let $x = \labeln(\rootn(\Z))$, construct
\begin{align*}
    \Z_0 \gets & 
    \begin{cases}
    \remove(\child{0}(\Z), R \setminus \{x\}) \cup \child{1}(\Z) & \text{if } x \in R,\\
    \remove(\child{0}(\Z), R \setminus \{x\}) & \text{if } x \notin R,\\
    \end{cases}\\
    \Z_1 \gets & \remove(\child{1}(\Z), R \setminus \{x\}),
\end{align*}
and just call and return $\mathsf{makenode}(x, \Z_0, \Z_1)$ (see the right of Fig.~\ref{fig:zdd}),
where $\mathsf{makenode}(x, \Z_0, \Z_1)$ is the following procedure:
If there is a node whose label is $x$ and whose $i$-arc points at the root of $\Z_i$ for $i = 0, 1$, just return the node.
Otherwise, make a new node with label $x$, make its $i$-arc point at the root of $\Z_i$ for $i = 0, 1$, and return the new node.


Next, we design an algorithm for $\add(\Z, A)$ for any $A \subseteq U$.
Note that there is a possibility that an element that never appears in $\Z$ but in $A$ is added to a set.
Let $x = \labeln(\rootn(\Z))$ and $y$ be the minimum element in $A$.
First, we consider the case of $x \ge y$.
Similarly to the $\remove$ operation, we call
$\mathsf{makenode}(x, \Z_0, \Z_1)$,
where
\begin{align*}
    \Z_0 \gets & \add(\child{0}(\Z), A \setminus \{x\}),\\
    \Z_1 \gets & 
    \begin{cases}
    \add(\child{1}(\Z), A \setminus \{x\}) \cup \child{0}(\Z), & \text{if } x \in A \\
    \add(\child{1}(\Z), A \setminus \{x\}) & \text{if } x \notin A.
    \end{cases}
\end{align*}
We consider the case of $x < y$, including the case where $\Z = \top$ and $A \neq \emptyset$,
which means that the constructed family contains sets obtained by adding $y$ to sets in $\sets(\Z)$.
In this case, we consider a ZDD $\Z'$ equivalent to
$\Z$ (i.e., $\sets(\Z') = \sets(\Z)$) such that $\labeln(\rootn(\Z')) = y$.
Such $\Z'$ is constructed
by calling $\mathsf{makenode}(y, \Z, \bot)$.
We then call and return $\add(\Z', A)$ recursively.

At the end of the recursion, $\add(\bot, A) = \bot$ for any $A \subseteq U$
and $\add(\top, \emptyset) = \bot$ (the case where $\add(\top, A)$ for a non-emptyset $A$ has already been described above).









\section{Versatility of the proposed algorithm}\label{sec:versatility}

In this section, we show the versatility of the proposed algorithm in the following three directions:
(i) By using $\Z^i$ (in Sec.~\ref{sec:framework_overview}), we can solve the variants introduced in Sec.~\ref{sec:reconf_problem} (discussed in Sec.~\ref{sec:variants}); (ii) By changing $\mathsf{op}(\Z)$ in equation (\ref{eq:z_i}), we can solve some models (in Sec.~\ref{sec:models});
(iii) By constructing $\zsol$, we can treat various reconfiguration objects and constraints (in Sec.~\ref{sec:objects}).

\subsection{Shortest, farthest, connectivity, and optimization variants}\label{sec:variants}

The ZDD $\Z^i$ represents the family of \emph{all} the independent sets that are reachable from the initial set $S$ in $i$ steps.
Therefore, the smallest integer $i$ such that $T \in \sets(\Z^i)$ holds
is the length of a shortest reconfiguration sequence from $S$ to $T$.
The proposed algorithm can solve not only the reachability variant but also the shortest one.

The shortest sequence $I_0\ (= S),\ldots,I_h\ (= T)$ between $S$ and $T$ can be obtained by
the following backtrack method, where $h$ is the smallest integer such that
$T \in \sets(\Z^h)$.
Here, we consider only the token jumping model; other models are similar.
Suppose that we have already obtained $I_p,\ldots,I_h$ $(2 \le p \le h)$.
Then, there are vertices $v \notin I_p$ and $w \in I_p$
such that $I_p \cup \{v\} \setminus \{w\} \in \sets(\Z^{p-1})$
according to the construction of $\Z^{p}$.
Thus, we let $I_{p-1} := I_p \cup \{v\} \setminus \{w\}$.
By the above method, we obtain $I_1,\ldots,I_h$.
Finally, it is obvious that $|I_0 \setminus I_1| = |I_1 \setminus I_0| = 1$ holds according to the construction of $\Z^1$,
which shows that the sequence $I_0,\ldots,I_h$ is certainly the reconfiguration sequence between $S$ and $T$.
The computation time is as follows.
We can test whether $I_p \cup \{v\} \setminus \{w\}$ is in $\sets(\Z^{p-1})$ or not
by a ZDD operation in $\mathrm{O}(|V|)$ time.
The number of candidates of $I_{p-1}$ is $\mathrm{O}(|V|^2)$.
Therefore, the computation time of obtaining the shortest sequence after constructing the ZDDs $\Z^{0},\ldots,\Z^h$ is $\mathrm{O}(h|V|^3)$.

Let us consider the farthest variant.
We construct $\Z^0,\Z^1,\ldots$ without checking $T \in \sets(\Z^{i})$ in the algorithm
until $\Z^{i} = \bot$ holds.
Let $h'$ be the smallest integer such that $\Z^{h'} = \bot$.
Then, a set in $\sets(\Z^{h'-1})$ is a farthest independent set from $S$.

We solve the connectivity variant based on the following idea.
If the solution space (graph) is connected, all the independent sets are reachable
from any set $S$.
Therefore, we randomly choose $S$ from $\sets(\zsol)$ by a ZDD operation and construct $\Z^0,\Z^1,\ldots,\Z^{h'-1}$ in the same way as the farthest variant.
Then, by examining whether
$\zsol$ is equivalent to $\bigcup_{i = 0,\ldots,h'-1} \Z^i$ or not,
we obtain the answer.
Note that checking the equivalency of two given ZDDs can be done in $\mathrm{O}(1)$ time
in many ZDD manipulation systems.

We can solve the optimization variant as follows, where the criterion of
the optimality is arbitrary as long as the optimal solution can be
extracted from a ZDD in polynomial time (e.g., the number of elements in the solution and the total weight of the solution~\cite{knuth:taocp41}).
Given a ZDD $\Z$, for each $i$,
we extract an optimal solution $J_i \subseteq U$ from $\sets(\Z^i)$.
Then, we choose the optimal one among $J_0,J_1,\ldots$
(if there are two or more such solutions with the same size, we choose one with minimum index).
By running the algorithm for the shortest variant that obtains a reconfiguration sequence from $S$ to the chosen solution,
we obtain the desired reconfiguration sequence.

We conclude this subsection by pointing out that our algorithm can solve
the reconfiguration problem with multiple start sets $S_1,\ldots,S_s$
and goal sets $T_1,\ldots,T_t$, where the task is to decide
whether a reconfiguration sequence between $S_j$ and $T_{j'}$ exists
for some $j, j'$ or not. Just let $\Z^0$ be the ZDD for
$\{S_1,\ldots,S_s\}$ and change deciding whether $T \in \sets(\Z^{i})$
into $T_{j'} \in \sets(\Z^{i})$ for some $j'$.


\subsection{Token jumping and token sliding models}\label{sec:models}

We consider the token jumping and token sliding models
by designing $\mathsf{op}(\Z)$ in equation (\ref{eq:z_i}).

The swap operation is to remove a vertex and add another vertex from and to an independent set, respectively.
For a ZDD $\Z$ (whose universal set is $U$) and sets $A, R \subseteq U$,
let $\swap(\Z, A, R)$ be the ZDD representing
\[
    \{ I \cup \{v\} \setminus \{v'\}
        \mid I \in \mathcal{S}(\Z), v \in A \setminus I, v' \in I \cap R \},
\]
which means that we add an element in $A$ and remove an element in $R$.
This can be represented by
$\add(\remove(\Z^{i-1}, R), A) \setminus \Z^{i-1}$.
The set subtraction of $\Z^{i-1}$ is needed because the  family represented by $\add(\allowbreak \remove(\Z^{i-1}, R), A)$ includes sets obtained by removing and adding the same vertex.

We can design a more efficient algorithm.
We only show $\Z_0$ and $\Z_1$ when calling $\mathsf{makenode}(x, \Z_0, \Z_1)$ with $x = \rootn(\Z)$.
The others are similar to the addition operation.
$\Z_0$ and $\Z_1$ are
\begin{align*}
    \Z_0 \gets &
    \begin{cases}
    \swap(\child{0}(\Z), A \setminus \{x\}, R \setminus \{x\}) \cup \add(\child{1}(\Z), A \setminus \{x\}), & x \in R, \\
    \swap(\child{0}(\Z), A \setminus \{x\}, R \setminus \{x\}) & x \notin R,
    \end{cases}\\
    \Z_1 \gets & 
    \begin{cases}
    \swap(\child{1}(\Z), A \setminus \{x\}, R \setminus \{x\}) \cup \remove(\child{0}(\Z), R \setminus \{x\}), & x \in A, \\
    \swap(\child{1}(\Z), A \setminus \{x\}, R \setminus \{x\}) & x \notin A.
    \end{cases}
\end{align*}
This holds because $\sets(\Z_0)$ includes the independent sets 
obtained by removing $x$ from each set in $\{\{x\}\} \Join \sets(\child{1}(\Z))$ and then adding a vertex other than $x$ if $x \in R$,
and $\sets(\Z_1)$ includes the independent sets
obtained by adding $x$ to each set in $\sets(\child{0}(\Z))$
and removing a vertex other than $x$ if $x \in A$.
At the end of the recursion, $\swap(\bot, A, R) = \swap(\top, A, R) = \bot$ holds for any $A$ and $R$.

The slide operation can be performed similarly to the swap operation.
Let $\mathsf{slide}(\Z)$ be the ZDD representing
\[
    \{ I \cup \{v\} \setminus \{v'\}
        \mid I \in \mathcal{S}(\Z), v \in V \setminus I, v' \in I, \{v, v'\} \in E \}.
\]
We only show $\Z_0$ and $\Z_1$ when calling $\mathsf{makenode}(x, \Z_0, \Z_1)$ with $x = \rootn(\Z)$.
For a vertex $v \in V$, let $N(v)$ be the set of neighbors of $v$;
that is, $N(v) = \{ w \in V \mid \{v, w\} \in E\}$.
Then,
\begin{align}
    \Z_0 \gets & \mathsf{slide}(\child{0}(\Z)) \cup \add(\child{1}(\Z), N(x)), \label{eq:slide_add} \\
    \Z_1 \gets & \mathsf{slide}(\child{1}(\Z)) \cup \remove(\child{0}(\Z), N(x)). \label{eq:slide_remove}
\end{align}
The reason the second argument in $\add$ and $\remove$ in equations (\ref{eq:slide_add}) and (\ref{eq:slide_remove}) is $N(v)$
is that the $\add$ (resp. $\remove$) operation is called with $\child{1}(\Z)$ (resp. $\child{0}(\Z)$), which means that we remove (resp. add) $x$ from (resp. to) $\sets(\Z)$ and thus we must add (resp. remove) a vertex adjacent to $x$.

The algorithm can solve the token sliding model for a directed graph~\cite{ito_et_al:LIPIcs.MFCS.2022.58}.
The slide operation on a directed graph can be designed
with a slight modification:
\begin{align*}
    \Z_0 \gets & \mathsf{slide}(\child{0}(\Z)) \cup \add(\child{1}(\Z), N^{+}(x)), \\
    \Z_1 \gets & \mathsf{slide}(\child{1}(\Z)) \cup \remove(\child{0}(\Z), N^{-}(x)),
\end{align*}
where $N^{+}(v)$ is the heads of the arcs outgoing from $v$
and $N^{-}(v)$ is the tails of the arcs incoming to $v$ for $v \in V$.


\subsection{Reconfiguration objects and constraints}\label{sec:objects}

The proposed algorithm does not depend on the characteristics of independent sets except for the construction of $\zsol$.
Therefore, when we want to solve some reconfiguration problem,
we can use the proposed algorithm
by presenting how to construct $\zsol$ for objects corresponding to the problem.
Many researchers have proposed ZDD construction algorithms for various set families, some of which can be applied to ZDD construction for many reconfiguration objects.
In this section, we overview what kinds of objects we can treat.

\subsubsection{Vertex subset}

We show that we can construct many kinds of objects each of which is represented as a subset of the vertex set by set operations. Assume that the universal set $U$ is $V$.

We begin with independent sets (although we mentioned in the previous section that there is a more efficient algorithm~\cite{Hayase1995}).
Let $\X_v$ and $\overline{\X}_v$ be respectively the family of all the sets including $v$ and the family of those not including $v$;
that is, $\X_v = \{ A \subseteq U \mid v \in A \}$
and $\X_v = \{ A \subseteq U \mid v \notin A \}$.
It is easy to construct ZDDs for $\X_v$ and $\overline{\X}_v$.
For two vertices $v$ and $w$, the family of all the sets including
at most one of $v$ and $w$ is $\overline{\X}_v \cup \overline{\X}_w$.
Therefore, the family of all the independent sets is
\[
    \bigcap_{\{v, w\} \in E} \left( \overline{\X}_v \cup \overline{\X}_w \right),
\]
and the ZDD for this family can be simply obtained by combining known ZDD operations~\cite{knuth:taocp41}.
Similarly, we can solve other reconfiguration objects by ZDD operations~\cite{knuth:taocp41}.
We show some of them in Table~\ref{tab:zdd_vertex_subset}.

\begin{table}[t]
\caption{Reconfiguration objects that can be represented as vertex subsets, and how to obtain them by set operations~\cite{knuth:taocp41}. Let $N_k(v)$ be the set of vertices whose distance from $v$ ranges from $1$ to $k$.}
\label{tab:zdd_vertex_subset}
\centering
\begin{tabular}{|l|l|} \hline
Reconfiguration object & Set operations \\ \hline\hline
Dominating set & $\bigcap_{v \in V} \left( \X_v \cup \left(\bigcup_{w \in N(v)}\X_w\right) \right)$ \\ \hline
Vertex cover & $\bigcap_{\{v,w\} \in E} \left( \X_v \cup \X_w \right)$ \\ \hline
Clique & $\bigcap_{\{v, w\} \notin E} \left( \overline{\X}_v \cup \overline{\X}_w \right)$ \\ \hline
Distance-$k$ independent set & $\bigcap_{v \in V} \bigcap_{w \in N_k(v)} \left( \overline{\X}_v \cup \overline{\X}_w \right)$ \\ \hline
Distance-$k$ dominating set & $\bigcap_{v \in V} \left( \X_v \cup \left(\bigcup_{w \in N_k(v)}\X_w\right) \right)$ \\ \hline
\end{tabular}
\end{table}

Coudert~\cite{582363} proposed algorithms that construct ZDDs representing the families of sets
obtained by collecting only the maximal/minimal sets in a family given as a ZDD $\Z$;
that is, $\mathsf{maximal}(\Z)$ is the ZDD for $\{ X \in \sets(\Z) \mid \forall X' \in \sets(\Z), X \subseteq X' \implies X = X' \}$ and $\mathsf{minimal}(\Z)$ is the ZDD for $\{ X \in \sets(\Z) \mid \forall X' \in \sets(\Z), X' \subseteq X \implies X = X' \}$.
Using the maximal operation, we can solve (the token jumping model of) the maximal independent set reconfiguration problem~\cite{CENSORHILLEL202085}, where every feasible solution of this problem is a maximal independent set.
We can also solve some maximal/minimal reconfiguration problems, such as
the minimal dominating set reconfiguration, the minimal vertex cover reconfiguration, and the maximal clique reconfiguration.

\if 0

In this subsection, we consider that the reconfiguration target is a vertex subset
such as an independent set.

We describe how to construct a ZDD representing the family of all the dominating sets.
(*** Write the definition of the dominating set here ***)
Let $D \subseteq V$ be a dominating set. For every vertex $v \in V$,
$v$ must be in $D$ or at least one of the neighbors of $v$ must be in $D$.

The family of sets that satisfy the above condition for $v$ is written by
\[
    X_v \cup \left(\bigcup_{u \in N(v)}X_u\right).
\]
The family of all the dominating sets is the family of sets that satisfy
the condition for all $v \in V$. Therefore, it is
\[
    \bigcap_{v \in V} \left( X_v \cup \left(\bigcup_{u \in N(v)}X_u\right) \right).
\]
Since the construction of $X_v$ is easy, the above family can be obtained
as a ZDD.

Next, we treat vertex covers. Consider an arbitrary vertex cover $C \subseteq V$.
For every edge $e = \{u, v\} \in E$, at least one of $u$ and $v$ is in $C$.
Therefore, the family of all the vertex covers is obtained by
\[
    \bigcap_{\{u, v\} \in E} \left( X_u \cup X_v \right).
\]

Next, we treat cliques. Consider an arbitrary clique $C \subseteq V$.
For every vertex pair $\{u, v\} \notin E$, both $u$ and $v$ must not be in $C$.
Therefore, the family of all the cliques is obtained by
\[
    \bigcap_{\{u, v\} \notin E} \left( \overline{X}_u \cup \overline{X}_v \right),
\]
where $\overline{X}_v = \{ U \subseteq X \mid v \notin U \}$.

Hogehoge proposed a method that constructs a ZDD representing the family of
hitting sets of a family represented by a given ZDD.
Using this, we obtain the families of $k$-path vertex cover,
feedback vertex sets, and odd cycle transversals as follows.
We construct ZDDs for paths with length $k$, cycles, and
cycles with odd length, and compute hitting sets of them.

Let $N_k(v)$ be the set of vertices whose distance from $v$ is at most $k$.
The family of distance-$r$ dominating sets is obtained by
\[
    \bigcap_{v \in V} \left( X_v \cup \left(\bigcup_{u \in N_r(v)}X_u\right) \right).
\]
The family of distance-$r$ independent sets is obtained by
\[
    \bigcap_{v \in V} \bigcap_{u \in N_r(v)} \left( \overline{X}_u \cup \overline{X}_v \right).
\]

\fi

\subsubsection{Subgraphs}

We consider a subgraph that can be represented by an edge set.
For example, a path can be represented by the set of edges consisting of the path.
Formally, for an edge set $E' \subseteq E$, a subgraph is represented by $(V', E')$,
where $V' = \bigcup_{\{v, w\} \in E'} (\{v\} \cup \{w\})$.
Then, we set the universe set $U$ to be $E$.
Note that we cannot treat subgraphs including isolated vertices in this representation.

Sekine et al.~\cite{Sekine1995} proposed an algorithm that constructs the ZDD
representing the family of all the spanning trees.
Knuth~\cite{knuth:taocp41} proposed a similar algorithm that constructs
the ZDD representing the family of all the $s$-$t$ paths.
Kawahara et al.~\cite{Kawahara2017} generalized their algorithms to
a framework that can treat various objects including matchings,
regular graphs, and Steiner trees,
and that can impose constraints such as the degree of each vertex, the connectivity of vertices, the existence of a cycle, and the number of edges (equal to, less than, or more than a specified value) in any combination.
Recent research for the construction of ZDDs enables us to
treat more complex graph classes such as degree constrained graphs~\cite{Kawahara2016},
chordal graphs~\cite{Kawahara2019}, interval graphs~\cite{Kawahara2019},
and planar graphs~\cite{Nakahata2020}. All of them can be treated as
reconfiguration objects and are shown in Fig.~\ref{fig:problems}. For example, the proposed algorithms can solve
the Steiner tree reconfiguration~\cite{DBLP:journals/ieicet/MizutaIZ17}, planar subgraph reconfiguration,
and so on.

The sliding model for edge sets can be considered by just changing the definition of the neighbor $N$ into $N(e) = \{ e' \mid e \text{ and } e' \text{ share an endpoint}  \}$.

\section{Experimental results}\label{sec:experiments} To check the performance of the proposed ZDD-based method,
we conducted an experimental comparison using the 1st place solver winning CoRe Challenge 2022. 

\noindent
\textbf{CoRe Challenge 2022.}
In 2022, the 1st Combinatorial Reconfiguration Challenge (CoRe Challenge 2022)\footnote{\url{https://core-challenge.github.io/2022/}} was held. 
CoRe Challenge 2022 is aiming for practically exploring the combinatorial reconfiguration. 
This 1st competition targets the token jumping model of the independent set reconfiguration problem~\cite{KaminskiMM12} and provides 369 instances including both instances that have a reconfiguration sequence (323 instances) and do not have any sequence (46 instances). 
Participated solvers include the state-of-the-art AI planner and BMC solvers based methods~\cite{DBLP:journals/corr/abs-2208-02495}, e.g., \textsf{SymK}~\cite{DBLP:conf/aaai/SpeckMN20} and \textsf{NuSMV}~\cite{CAV02}.

\noindent
\textbf{Experimental Condition.}
We compare our system with \textsf{recon} (@telematik-tuhh)~\cite{recon} which is based on a hybridization of the IDA* algorithm and the breadth-first search. It found 280 shortest reconfiguration sequences and became the 1st place solver of the overall solver track of the shortest reconfiguration metric\footnote{\url{https://core-challenge.github.io/2022result/}}. Except for \texttt{queen} benchmark series, instances solved by \textsf{recon} contain all instances solved by the 2nd and the 3rd place solvers. 
We compared how many shortest reconfiguration sequences can be found by each system.
We use a machine that equips a 2.30 GHz CPU and 2 TB RAM. 
\KJ{}{The proposed ZDD solver is written in C++ language with the SAPPOROBDD\footnote{\url{https://github.com/Shin-ichi-Minato/SAPPOROBDD}} and TdZdd~\cite{iwashita2013efficient} libraries and compiled by \texttt{g++} with \texttt{-O3} option.
The variable of ZDDs is ordered by the heuristic described in \cite{Fifield2020}.
The implementation of the proposed algorithm
and the scripts that reproduce the experiments are published at the GitHub page\footnote{\url{https://github.com/junkawahara/ddreconf-experiments2023}}.}

\noindent
\textbf{Results.}
Table~\ref{tab:exp1} shows comparisons between the proposed algorithm and the 1st place solver \textsf{recon} for each series of the benchmark instances. 
\KJ{}{In this experiment, the time limit is two hours.}
The 1st and 2nd columns denote the name of the benchmark series and the number of instances included in each series, respectively.
The 3rd and 4th columns denote the maximum number of vertices and edges in each series, respectively.
The longest shortest reconfiguration length known in each series is shown in the 5th column.
The 6th and 7th columns denote the number of instances solved by the two methods. 
Benchmark series are sorted in the order of the longest shortest reconfiguration length.

From this table, we can read \KJ{there are}{}pros/cons of the proposed algorithm and \textsf{recon}. The proposed algorithm is good at solving the instances having long reconfiguration sequences but not so good instances of large-sized graphs. The \textsf{recon} solver can \KJ{adopt}{adapt} instances of large-sized graphs but cannot solve \KJ{}{many of} instances having long reconfiguration sequences.
One of the major bottlenecks of the proposed algorithm is constructing the ZDD $\zind$ representing all the independent sets.
If the graph is large (e.g., the number of edges is more than 10{,}000), it takes a very long time and large memory to construct $\zind$.
Table~\ref{tab:exp2} shows the results classified by the length of the shortest reconfiguration found. This table shows more clearly the characteristics of the two methods.

Figure~\ref{fig:sp-cpu} shows a plot showing the relation of the length of the shortest reconfiguration sequence found and CPU time in log scale for \texttt{sp} series.
\KJ{}{In this experiment, to confirm how long the reconfiguration sequences that algorithms can find are, we set the time limit to be 200{,}000 seconds.}
We can read that the CPU time of the proposed algorithm rises gently with respect to the length, while \textsf{recon} rises steeply. Figure~\ref{fig:sp-memory} shows a similar plot, but we compare memory usage. The proposed algorithm uses the memory at the beginning for the ZDD library, but the situation reverses when the reconfiguration sequence becomes longer.
\KJ{}{The proposed algorithm succeeded in 
 computing the shortest sequence with length 5{,}767{,}157 for \texttt{sp019} instance with 247 vertices and 1{,}578 edges in 151{,}567 seconds.
In the proposed algorithm for \texttt{sp019}, the size (number of nodes) of the ZDDs $\Z^i$ for each $i$ is at most tens of thousands, but some of them contain more than $10^{10}$ independent sets.
The proposed algorithm behaves as if it searched the solution space like a breadth-first search
while compressing found solutions.
This indicates that the proposed algorithm is good at instances where the width of the solution space is relatively small, but the length of it is very long.
The \textsf{recon} solver also conducts the breadth-first search, but it takes a long time because the solution space itself is enormous.
}

\begin{table}
\caption{Experimental results for each series}
\label{tab:exp1}
\centering
\begin{tabular}{|l|r|r|r|r|r|r|} \hline
Dataset & \# Inst. & Max $|V|$ & Max $|E|$ & Reconf len & \# Solved ZDD & \# Solved recon \\ \hline \hline
\texttt{grid} & 4 & 40000 & 79600 & 8 & \textbf{2} & \textbf{2}\\ \hline
\texttt{handcrafted} & 5 & 36 & 51 & 69 & \textbf{5} & \textbf{5}\\ \hline
\texttt{color04} & 202 & 10000 & 990000 & 112 & 76 & \textbf{201}\\ \hline
\texttt{queen} & 48 & 40000 & 13253400 & 159 & 8 & \textbf{40}\\ \hline
\texttt{square} & 17 & 204 & 303 & 1722 & \textbf{17} & 8\\ \hline
\texttt{power} & 17 & 304 & 463 & 55139 & \textbf{11} & 6\\ \hline
\texttt{sp} & 30 & 390 & 2502 & 90101 & \textbf{15} & 10\\ \hline
\end{tabular}
\end{table}

\begin{table}
\caption{Experimental results for each range of reconfiguration lengths}
\label{tab:exp2}
\centering
\begin{tabular}{|r|r|r|r|} \hline
Reconf len $\ell$ & \# Instances & \# Solved ZDD & \# Solved recon \\ \hline \hline
$1 \le \ell \le 10$ & 178 & 70 & \textbf{178}\\ \hline
$10 < \ell \le 100$ & 78 & 25 & \textbf{73}\\ \hline
$100 < \ell \le 1000$ & 21 & \textbf{16} & 13\\ \hline
$1000 < \ell \le 10000$ & 11 & \textbf{11} & 6\\ \hline
$10000 < \ell \le 100000$ & 7 & \textbf{7} & 2\\ \hline
\end{tabular}
\end{table}




\begin{figure}[tb]
  \begin{minipage}{0.49\hsize}
    \centering
  \includegraphics[width=\textwidth]{fig_sp_time.pdf}
  \caption{Time for \texttt{sp} series.}
    \label{fig:sp-cpu}
  \end{minipage}  \begin{minipage}{0.02\hsize}
  \quad
  \end{minipage}
  \begin{minipage}{0.49\hsize}
    \centering
  \includegraphics[width=\textwidth]{fig_sp_memory.pdf}
  \caption{Memory usage for \texttt{sp} series.}
    \label{fig:sp-memory}
  \end{minipage}\end{figure}


\if 0

\section{Applications of the Framework and Experimental Evaluations}

In this section, we apply our ZDD-based algorithmic framework to three types of shortest reconfiguration problems, which have different complexity status: PSPACE-hard, NP-hard and P. 

\subsection{Shortest independent set reconfiguration}
The reachability variant of independent sets (and hence its shortest variant) is known to be PSPACE-complete~\cite{KaminskiMM12}. 

Let $S$ and $T$ be independent sets.
First, we construct a ZDD $\mathcal{U}_{\mathrm{ind}}$ that represents the set of all the
independent sets of $G$ by an algorithm in~\cite{Hayase1995} or an algorithm in~\cite[p.231]{knuth:taocp41}.
Then, by calling $\mathsf{FindReconfSequence}(\mathcal{U}_{\mathrm{ind}}, V, S, T)$,
we obtain the output.

\subsection{Shortest matching reconfiguration}
The shortest variant of matchings is NP-hard for bipartite graphs of maximum degree three~\cite{BHIM19}, while the reachability variant of matchings is solvable in polynomial time for general graphs~\cite{IDHPSUU11}. 

Let $S$ and $T$ be matchings.
First, we construct a ZDD $\mathcal{U}_{\mathrm{mat}}$ that represents the set of all the
matchings of $G$ by the algorithm in~\cite{Kawahara2017}.
Then, by calling $\mathsf{FindReconfSequence}(\mathcal{U}_{\mathrm{mat}}, E, S, T)$,
we obtain the output.

\subsection{Shortest spanning tree reconfiguration}
The shortest variant of spanning trees is solvable in polynomial time~\cite{IDHPSUU11}. 

Let $S$ and $T$ be spanning trees.
First, we construct a ZDD $\mathcal{U}_{\mathrm{spt}}$ that represents the set of all the
spanning trees of $G$ by the algorithm in~\cite{Sekine1995}.
Then, by calling $\mathsf{FindReconfSequence}(\mathcal{U}_{\mathrm{spt}}, E,\allowbreak{} S,\allowbreak{} T)$,
we obtain the output.

\fi

\if 0

\section{Theoretical Analysis for Operations of ZDD-Based Algorithm}\label{sec:analysis}

In this section, we give the theoretical analysis of the running time
for operations $\remove$, $\add$, $\swap$. 
We show that these operations require at least subexponential time\footnote{
We say that an algorithm is a {\it subexponential time} algorithm
if its running time is $2^{o(n)}$ for the input size $n$.} in the worst case. 

\begin{lemma}\label{lem:remove_time} 
The operation $\remove$ requires at least subexponential time
in the worst case. 
\end{lemma}

Lemma~\ref{lem:remove_time} is derived from the following lemma 
which implies that the size of ZDD can become subexponentially large by operation $\remove$.

\begin{lemma}\label{lem:remove_size}
There exists a family $\mathcal{F}$ with universal set $X = \{x_1, \ldots, x_n\}$ such that
$|{\rm ZDD}(\mathcal{F})| = O(n^2)$ and $|{\rm ZDD}(\remove(\mathcal{F}))| = \Omega(2^{n/3})$.
\end{lemma}

\begin{proof}[Proof of Lemma~\ref{lem:remove_time}.]
By Lemma~\ref{lem:remove_size}, there exists a family $\mathcal{F}$ 
such that the size of output by $\remove$ is $\Omega\left(2^{\sqrt{|\text{ZDD}(\mathcal{F})|}/3}\right)$. 
Thus, $\remove$ requires at least subexponential time only to output the result in the worst case.
\end{proof}

\begin{proof}[Proof of Lemma~\ref{lem:remove_size}.]
Let us suppose that the size $n$ of the universal set $X$ is a multiple of three, and $n = 3m$. 
(For the other case, we can show similarly by setting that $m$ is a quotient of $n$ and three.)
Let $X_1$ denote a set of $m$ elements $\{x_1, x_2, \ldots, x_m\}$. 
Similarly, let $X_2$ and $X_3$ denote sets $\{x_{m+i} \mid 1 \leq i \leq m \}$ 
and $\{x_{2m+i} \mid 1 \leq i \leq m \}$, respectively. 
We sometimes use $[m]$ to denote a set $\{1,2,\ldots, m\}$. 

We show that the following family $\mathcal{F}$ satisfies the statement of the lemma: 
\[
{\cal F} = \bigcup_{i \in \{1,\ldots, m\}} \{ \{x_i\} \} \Join 2^{F^{-}_{m+i}} \Join \{ \{x_{2m+i}\} \},
\text{ where } F^{-}_{k} := X_2 \backslash \{x_{k}\} \text{ for integer } k.
\]

First, we show that the size (or the number of nodes) of ZDD($\mathcal{F}$) is at most $O(n^2)$
by giving a concrete construction as follows: 
Prepare $m$ non-terminal nodes $\nu_1, \ldots, \nu_m$.
For each $i \in \{1, \ldots, m\}$, node $\nu_i$ has a label $x_i$.
For each $i$ where $1 \leq i \leq m-1$, 0-arc of $\nu_i$ points at $\nu_{i+1}$, and one of $\nu_{m}$ points at $\bot$.
On the other hand, 1-arc of $\nu_i$ points at the root of a ZDD that represents 
a family $2^{F^{-}_{m+i}} \Join \{ \{x_{2m+i}\} \}$, 
denoted by $Z_i$. 
We will show that one can construct such $Z_i$ of the size $m$. 
It implies that the total of the size of our ZDD is $m + m^2 = O(n^2)$, and then the first step of the proof is complete.

Thus, the rest of the first step is to give the construction of ZDD $Z_i$
that represents $2^{F^{-}_{m+i}} \Join \{ \{x_{2m+i}\} \}$
such that its size is $m$.
From a fundamental property of ZDD, for any universal set $Y$ with $\ell$ elements, 
a power set of $2^{Y}$ can be represented by a ZDD of the size $\ell$.\footnote{
The construction of a power set $2^Y$ for $Y = \{y_1, y_2, \ldots, y_\ell\}$ is as follows:
Prepare $\ell$ non-terminal nodes $\nu_1, \ldots, \nu_\ell$ and each node $\nu_i$ has a label $y_i$ for each $i \in [\ell]$.
For each $i$ where $1 \leq i \leq \ell-1$, 
both of 0-arc and 1-arc of node $\nu_i$ point at node $\nu_{i+1}$,
and both arcs of node $\nu_\ell$ point at $\top$.}
Therefore, a family $2^{F^{-}_{m+i}}$ is represented by a ZDD of the size $m-1$ and let $Z'_i$ denote such a ZDD. 
We obtain $Z_i$ by modifying $Z'_i$ as follows:
Add an extra non-terminal node $\nu'$ with label $x_{2m+i}$ whose 0-arc points at $\bot$ and 1-arc points at $\top$,
and reorient both of 0-arc and 1-arc of the bottom non-terminal node in $Z'_i$ 
to point at $\nu'$. 
Thus, this $Z_i$ represents $2^{F^{-}_{m+i}} \Join \{ \{x_{2m+i}\} \}$ and its size is $m$, and the first step of the proof is done.

Next, we show that the size of ZDD($\remove(\mathcal{F})$) is $\Omega(2^{n/3})$. 
A family $\remove(\mathcal{F})$ can be represented by the following equation:
\begin{eqnarray}\label{eq:family_rem_F}
\remove(\mathcal{F}) & = & 
\left( \bigcup_{i \in [m]} 2^{F^{-}_{m+i}} \Join \{ \{x_{2m+i}\} \} \right) \nonumber \\
& & \cup
\left( \bigcup_{i \in [m]} \{ \{x_i\} \} \Join \remove( 2^{F^{-}_{m+i}} \Join \{ \{x_{2m+i}\} \} ) \right).
\end{eqnarray}
The first term of \eqref{eq:family_rem_F} contains all sets that obtained by removing an element $x \in \{x_1, ..., x_m\}$ from all sets in $\mathcal{F}$.
The second term contains all sets that obtained by removing an element except for $x_1, ..., x_m$ from all sets in $\mathcal{F}$. 
Let $\mathcal{G}$ be a family of the first term of \eqref{eq:family_rem_F}, that is, 
$\mathcal{G} := \bigcup_{i \in [m]} 2^{F^{-}_{m+i}} \Join \{ \{x_{2m+i}\} \}$. 
Because any set in $\remove(\mathcal{F}) \setminus \mathcal{G}$ contains one of $\{x_1, \ldots, x_m\}$, 
$\text{ZDD}(\remove(\mathcal{F}))$ should contain an exact copy of $\text{ZDD}(\mathcal{G})$.
Thus, $|\text{ZDD}(\remove(\mathcal{F}))| \geq |\text{ZDD}(\mathcal{G})|$ holds. 
Therefore, it is enough to show that $|\text{ZDD}(\mathcal{G})| = \Omega(2^{n/3})$. 

To estimate the size of $\text{ZDD}(\mathcal{G})$, we give another representation of $\mathcal{G}$. 
\begin{lemma}\label{lem:g_rep}
Let $\mathcal{G}$ be a family $\bigcup_{i \in [m]} 2^{F^{-}_{m+i}} \Join \{ \{x_{2m+i}\} \}$.
Then, we also have
\begin{eqnarray}\label{eq:family_G}
\mathcal{G} &=& \bigcup_{I \subset [m]}
\{ \{x_{m+i} \mid i \in I\} \} \Join \{ \{x_{2m+j}\} \mid j \in [m]\setminus I\} \nonumber \\
&=& \bigcup_{I \subset [m]} \bigcup_{j \in [m]\setminus I }
\{ \{x_{m+i} \mid i \in I\} \cup \{x_{2m+j}\} \}.
\end{eqnarray}
\end{lemma}
\begin{proof}

Let $\mathcal{G'} := \bigcup_{I \subset [m]} \bigcup_{j \in [m]\setminus I }
\{ \{x_{m+i} \mid i \in I\} \cup \{x_{2m+j}\} \}$. 
First, we show that $\mathcal{G} \subseteq \mathcal{G'}$ holds.
Let $G$ be a set in family $\mathcal{G}$. 
By the definition of $\mathcal{G}$, we have $G = G' \cup \{x_{2m+j}\}$ for some $j$, 
where $G'$ is a set in $2^{F^{-}_{m+j}}$ and $1 \leq j \leq m$. 
Letting $I$ be a set $\{i \mid x_{m+i} \in G'\}$, we have $G' = \{x_{m+i} \mid i \in I \}$. 
Since $G' \in 2^{F^{-}_{m+j}}$ holds, we have $x_{m+j} \notin G'$ and thus $j \notin I$ holds. 
Therefore, we have $j \in [m] \setminus I$ and $G = \{x_{m+i} \mid i \in I \} \cup \{x_{2m+j}\} \in \mathcal{G'}$.
Thus, $\mathcal{G} \subseteq \mathcal{G'}$ holds. 

The rest of the proof is to show that $\mathcal{G'} \subseteq \mathcal{G}$ holds.
Let $G$ be a set in family $\mathcal{G'}$. 
By the definition of $\mathcal{G'}$, we have $G = \{x_{m+i} \mid i \in I\} \cup \{x_{2m+j}\}$ 
for some $I \subset [m]$ and $j \in [m]\setminus I$. 
Since $j \notin I$ holds, $\{x_{m+i} \mid i \in I\}$ dose not contain $x_{m+j}$. 
Therefore, $\{x_{m+i} \mid i \in I\}$ is a set in $2^{F^{-}_{m+j}}$
and it means that $G$ is contained in $\mathcal{G}$. 
Thus, $\mathcal{G'} \subseteq \mathcal{G}$ and the proof is complete.
\end{proof}

Lemma~\ref{lem:g_rep} implies that $\text{ZDD}(\mathcal{G})$ needs to distinguish sets
$\{ x_{m+i} \mid i \in I \}$ for each $I \subset [m]$ at level $2m+1$. 
That is, any pair of edges that go through between levels $2m$ and $2m+1$ does not join at the same node.
This means that the number of nodes of $\text{ZDD}(\mathcal{G})$ is at least $2^{m} - 1 = 2^{n/3} - 1$. 
Therefore, $|\mathrm{ZDD}(\mathcal{G})|$ (and also $|\mathrm{ZDD}(\remove(\mathcal{F}))|$) is $\Omega(2^{n/3})$.
\end{proof}

To give the running time of the operation $\add$, 
we also give the lemma about the rate of change of the size of ZDD by $\add$.

\begin{lemma}\label{lem:add_size}
There exists a family $\mathcal{F}$ with universal set $X = \{x_1, \ldots, x_n\}$ such that
$|\mathrm{ZDD}(\mathcal{F})| = O(n^3)$ and $|\mathrm{ZDD}(\add(\mathcal{F}))| = \Omega(2^{n/3}/n)$.
\end{lemma}
\begin{proof}
Let $\mathcal{G}$ be a family that the statement of Lemma~\ref{lem:remove_size} holds.
Now, we set a family $\mathcal{F}$ as a family of complements of all sets in $\mathcal{G}$, 
that is, $\mathcal{F} := \{S^c \mid S \in \mathcal{G}\}$. 
We apply the fact that the ratio of $|\mathrm{ZDD}(\mathcal{F})|$ to $|\mathrm{ZDD}(\mathcal{G})|$ is at most $n$. 
In fact, one can construct $|\mathrm{ZDD}(\mathcal{F})|$ as follows: 
Base operation is to switch each 1-arc with 0-arc, and vice versa. 
However, if there exists a 0-arc from a node with label $x_i$ to another node with label $x_j$ where $i + 1 < j$, 
then we replace this 0-arc with consecutive nodes with labels $x_i, x_{i+1}, x_{i+2}, \ldots, x_j$
connected by 0-arcs as an intermediate operation. 
By this operation, any path from the root to $\top$ of ZDD($\mathcal{G}$) that represents a set $S \in \mathcal{G}$
is changed to a path that represents its complement set $S^c \in \mathcal{F}$.
Thus, we have $|\mathrm{ZDD}(\mathcal{F})| \leq n \cdot |\mathrm{ZDD}(\mathcal{G})| = O(n^3)$. 

Now, to give the lower bound of $|\mathrm{ZDD}(\add(\mathcal{F}))|$, 
we show that if $S \in \remove(\mathcal{G})$ then its complement $S^c$ is contained in $\add(\mathcal{F})$.
Since $S \in \remove(\mathcal{G})$, there is an element $x \notin S$ such that $S \cup \{x\} \in \mathcal{G}$.
By the definition of $\mathcal{F}$, $(S \cup \{x\})^c \in \mathcal{F}$ holds and then $(S \cup \{x\})^c \cup \{x\} \in \add(\mathcal{F})$ holds 
because $(S \cup \{x\})^c$ dose not contain $x$. Moreover, $(S \cup \{x\})^c \cup \{x\}$ is exactly $S^c$. 
Therefore, we have $\add(\mathcal{F}) = \{S^c \mid S \in \remove(\mathcal{G})\}$
and then $|\mathrm{ZDD}(\add(\mathcal{F}))| \geq |\mathrm{ZDD}(\remove(\mathcal{G}))| / n = \Omega(2^{n/3}/n)$ holds.
\end{proof}

Lemma~\ref{lem:add_size} implies that the following.
\begin{lemma}\label{lem:add_time} 
The operation $\add$ requires at least subexponential time in the worst case. 
\end{lemma}

Because the operation $\swap$ calls $\remove$ and $\add$ as sub-modules,
Lemmas~\ref{lem:remove_time} and~\ref{lem:add_time} imply the following result 
for the running time of the main operation of our algorithm. 

\begin{theorem}\label{lem:swap_time} 
The operation $\swap$ requires at least subexponential time in the worst case. 
\end{theorem}

\fi

\section{Conclusion}\label{sec:conclusion}

We have proposed a ZDD-based framework for solving combinatorial reconfiguration problems.
We have shown that the framework can treat various reconfiguration objects, described in Fig.~\ref{fig:problems}.
The framework can solve the TAR and jumping models and the sliding model on a (directed) graph.
We have also shown that our framework is used for analyzing the solution space of reconfiguration problems such as the reachability, shortest, farthest, connectivity, and optimization variants.
We are trying to implement all of the features described in the paper,
and some of them have already been published at the website\footnote{\url{https://github.com/junkawahara/ddreconf}}.
Currently, the program can treat independent/dominating sets, matchings, (spanning/Steiner) trees, and forests as reconfiguration objects under the TAR, token jumping, and token sliding models.
We hope that these features will contribute to analyzing reconfiguration problems from theoretical and practical points of view.

Future work includes theoretically analyzing the complexity of the proposed algorithm,
designing ZDD-based algorithms for problems for which the solution space cannot be directly represented as a set family,
such as coloring reconfiguration problems~\cite{Cereceda2008} and graph partition reconfiguration problems~\cite{https://doi.org/10.1002/jgt.22856},
and applying the algorithm to practical problems.

\if 0

\appendix

\section{Proofs of the correctness of algorithms}


For $x \in \{ y \mid y \in F \in \mathcal{F} \}$,
we decompose $\mathcal{F}$ into the families the member of which includes and does not include $x$.
Let $\mathsf{decomp}_0(\mathcal{F}, x) = \{ F \mid F \in \mathcal{F}, x \notin F \}$ and
$\mathsf{decomp}_1(\mathcal{F}, x) = \{ F \setminus \{x\} \mid F \in \mathcal{F}, x \in F \}$.
Then, $\mathcal{F} = \mathsf{decomp}_0(\mathcal{F}, x) \cup (\{\{x\}\} \Join \mathsf{decomp}_1(\mathcal{F}, x))$.

To compute $\remove$, we use the following recursive structure:
\begin{lemma}\label{lem:rem}
If $\mathcal{F} \neq \emptyset$ and $\mathcal{F} \neq \{\emptyset\}$,
\begin{eqnarray*}
    \mathsf{decomp}_0(\remove(\mathcal{F}), x)
     & = & \remove(\mathsf{decomp}_0(\mathcal{F}, x)) \cup \mathsf{decomp}_1(\mathcal{F}, x), \\
     \mathsf{decomp}_1(\remove(\mathcal{F}), x)
     & = & \remove(\mathsf{decomp}_1(\mathcal{F}, x)).
\end{eqnarray*}
\end{lemma}

\begin{proof}
We prove $\mathsf{decomp}_0(\remove(\mathcal{F}), x)
     \subseteq  \remove(\mathsf{decomp}_0(\mathcal{F}, x)) \cup \mathsf{decomp}_1(\mathcal{F}, x)$.
We take $A \in \mathsf{decomp}_0(\remove(\mathcal{F}), x)$.
We consider two cases: (i) $A$ is obtained by removing $x$ from a set $B \in \mathcal{F}$, where $x \in B$, and (ii) $A$ is obtained by removing $y$ from a set $B' \in \mathcal{F}$, where $x \notin B'$ and $y \in B'$.
In case (i), $A \in \mathsf{decomp}_1(\mathcal{F}, x)$ holds because $B \in \mathcal{F}$ and an element in $\mathsf{decomp}_1(\mathcal{F}, x)$ is obtained by removing $x$ from a set in $\mathcal{F}$ that includes $x$.
In case (ii), $A \in \remove(\mathsf{decomp}_0(\mathcal{F}, x))$ holds because $B' \in \mathsf{decomp}_0(\mathcal{F}, x)$ and $A$ is a set obtained by removing an element from $B'$.
Therefore, $A \in \remove(\mathsf{decomp}_0(\mathcal{F}, x)) \cup \mathsf{decomp}_1(\mathcal{F}, x)$ holds, which proves $\mathsf{decomp}_0(\remove(\mathcal{F}), x)
     \subseteq  \remove(\mathsf{decomp}_0(\mathcal{F}, x)) \cup \mathsf{decomp}_1(\mathcal{F}, x)$.

We prove $\remove(\mathsf{decomp}_0(\mathcal{F}, x)) \cup \mathsf{decomp}_1(\mathcal{F}, x)
     \subseteq \mathsf{decomp}_0(\remove(\mathcal{F}), x)$.
We take $A \in \remove(\mathsf{decomp}_0(\mathcal{F}, x))$. Then, $x \notin A$ holds. There exists $y\ (\neq x)$ such that $A \cup \{y\} \in \mathsf{decomp}_0(\mathcal{F}, x)$. Thus, $A \in \remove(\mathcal{F})$ and since $x \neq A$, $A \in \mathsf{decomp}_0(\remove(\mathcal{F}), x)$.
Next, we take $A' \in \mathsf{decomp}_1(\mathcal{F}, x)$. Then, $A' \cup \{x\} \in \mathcal{F}$ holds, and thus $A' \in \remove(\mathcal{F})$ holds. Since $x \notin A'$, $A' \in \mathsf{decomp}_0(\remove(\mathcal{F}), x)$, which proves $\remove(\mathsf{decomp}_0(\mathcal{F}, x)) \cup \mathsf{decomp}_1(\mathcal{F}, x)
     \subseteq \mathsf{decomp}_0(\remove(\mathcal{F}), x)$.
     
We prove $\mathsf{decomp}_1(\remove(\mathcal{F}), x)
      \subseteq \remove(\mathsf{decomp}_1(\mathcal{F}, x))$.
We take $A \in \mathsf{decomp}_1(\remove(\mathcal{F}), x)$. Then, $A \cup \{x\} \in \remove(\mathcal{F})$, and thus $A \cup \{x, y\} \in \mathcal{F}$ for some $y \neq x$.
$A \cup \{y\} \in \mathsf{decomp}_1(\mathcal{F}, x)$ and $A \in \remove(\mathsf{decomp}_1(\mathcal{F}, x))$.

We prove $\remove(\mathsf{decomp}_1(\mathcal{F}, x))
      \subseteq \mathsf{decomp}_1(\remove(\mathcal{F}), x) $.
We take $A' \in \remove(\mathsf{decomp}_1(\mathcal{F}, x))$.
Then, there exists $y \neq x$ such that $A' \cup \{y\} \in \mathsf{decomp}_1(\mathcal{F}, x)$. $A' \cup \{x, y\} \in \mathcal{F}$. $A' \cup \{x\} \in \remove(\mathcal{F})$. $A' \in \mathsf{decomp}_1(\remove(\mathcal{F}), x)$.
\end{proof}

We use the recursive structure of ZDDs. Let $\mathcal{Z}$ be a ZDD.
For $i = 0, 1$, let $\nu_i$ be the node pointed at by the $i$-arc of $\rootn(\mathcal{Z})$.
We regard the DAG consisting of all the nodes and arcs reachable from $\nu_i$
as a ZDD, and let $\mathcal{Z}_i$ be the ZDD. Then, we can easily confirm that
$\mathcal{Z}_i = \mathsf{decomp}_i(\mathcal{F}, \rootn(\mathcal{Z}))$.
We often identify a node and the ZDD consisting of all the nodes and arcs reachable
from the node.

On the basis of the recursive structure of ZDDs and Lemma~\ref{lem:rem},
we design a recursive algorithm for constructing a ZDD for $\remove(\mathcal{F})$.
Here, $\remove(\mathcal{F})$ returns the root node of a ZDD.
Lemma~\ref{lem:rem} tells us that the 0-child of the constructed ZDD $\remove(\mathcal{F})$
represents the family $\remove(\mathsf{decomp}_0(\mathcal{F}, x)) \cup \mathsf{decomp}_1(\mathcal{F}, x)$ and the 1-child represents $\remove(\mathsf{decomp}_1(\mathcal{F}, x))$.
As the above discussion, recall that $\mathcal{Z}_i = \mathsf{decomp}_i(\mathcal{F}, \rootn(\mathcal{Z}))$.
First, we create the new root node with the label same as $\rootn(\mathcal{Z})$, say $x$,
and its 0-arc and 1-arc.
Then, we recursively call $\remove(\mathcal{F}_0)$ and take the union of
the returned ZDD and $\mathcal{F}_1$. We make the new 0-arc point at (the root of) the obtained ZDD.
Next, we recursively call $\remove(\mathcal{F}_1)$ and
make the new 1-arc point at (the root of) the obtained ZDD.
If $\mathcal{F} = \emptyset$ or $\mathcal{F} = \{\emptyset\}$, it returns $\bot$,
which means $\emptyset$. Since this algorithm is similar to one we will design
for $\swap$ later, we omit pseudocode for $\remove$,
and instead we will show pseudocode for $\swap$.

\begin{lemma}
Assume that $\mathcal{F} \neq \emptyset$ and $\mathcal{F} \neq \{\emptyset\}$.
If $x \in A$, then
\begin{eqnarray*}
    \mathsf{decomp}_0(\add(\mathcal{F}, A), x)
     & = & \add(\mathsf{decomp}_0(\mathcal{F}, x), A \setminus \{x\}) , \\
     \mathsf{decomp}_1(\add(\mathcal{F}, A), x)
     & = & \mathsf{decomp}_0(\mathcal{F},x)  \cup \add(\mathsf{decomp}_1(\mathcal{F}, x), A \setminus \{x\}).
\end{eqnarray*}
Otherwise $(x \notin A)$,
\begin{eqnarray*}
    \mathsf{decomp}_0(\add(\mathcal{F}, A), x)
     & = & \add(\mathsf{decomp}_0(\mathcal{F}, x), A) , \\
     \mathsf{decomp}_1(\add(\mathcal{F}, A), x)
     & = & \add(\mathsf{decomp}_1(\mathcal{F}, x), A).
\end{eqnarray*}
\end{lemma}

The difference of $\remove$ and $\add$ is that
we must specify a set $A$ for $\add$, which represents
elements that we can add to each set in $\mathcal{F}$.
Note that the order of variables in ZDDs must respect one
determined in advance, that is, for two ZDD nodes $\nu$ and
$\nu'$, if $\nu$ points at $\nu'$ (by its 0-arc or 1-arc),
$\labeln(\nu) < \labeln(\nu')$ must hold.
Therefore, when adding an element in $A$ to a set in a family
in the process of the recursive procedure we will describe below,
we must consider the order of nodes.

First, we consider the non-terminal cases where
$\mathcal{F} \neq \emptyset$ and $\mathcal{F} \neq \{\emptyset\}$ hold.
Let $x = \labeln(\rootn(\mathcal{F}))$ and $y = \min(A)$.
We divide three cases: (i) $x = y$, (ii) $x < y$, and (iii) $x > y$.
(i) If $x = y$, $x \in A$ holds. It is similar to the above procedure for $\remove$.
Namely, we recursively call $\add(\mathcal{F}_0, A \setminus \{x\})$
as a 0-child of the new root and the union of $\add(\mathcal{F}_1, A \setminus \{x\})$
and $\mathcal{F}_0$ as a 1-child of the new root.
(ii) If $x < y$, this means that $x \not \in A$ and
thus we cannot add $x$ or an element smaller than $x$ to any set in $\mathcal{F}$.
Hence, we just make recursive calls of $\add(\mathcal{F}_0, A)$ and
$\add(\mathcal{F}_1, A)$, create the root node with label $x$,
and make its 0-arc and 1-arc point at the (root of) obtained ZDDs.
(iii) If $x > y$, this means that $x \not \in A$ but
we cannot add an element smaller than $x$ to a set in $\mathcal{F}$.
Therefore, we create a node $\nu$ with label $y$ and its 0-arc and 1-arc.
We recursively call $\add(\mathcal{F}_0, A \setminus \{y\})$
as a 0-child of $\nu$. We make the 1-arc of $\nu$ point at ZDD $\mathcal{F}$.
The rest we should consider is the terminal cases. If $\mathcal{F} = \emptyset$,
just return $\bot$. If $\mathcal{F} = \{\emptyset\}$,
recall that $\add(\{\emptyset\}, A) = \{ \{x\} \mid x \in A \}$.
It is easy to construct a ZDD representing
$\{ \{x\} \mid x \in A \}$.

\begin{lemma}
Assume that $\mathcal{F} \neq \emptyset$ and $\mathcal{F} \neq \{\emptyset\}$.
If $x \in A$, then
\begin{eqnarray*}
    \mathsf{decomp}_0(\swap(\mathcal{F}, A), x)
     & = & \swap(\mathsf{decomp}_0(\mathcal{F}, x), A \setminus \{x\}) \cup  \add(\mathsf{decomp}_1(\mathcal{F}, x), A \setminus \{x\}), \\
     \mathsf{decomp}_1(\swap(\mathcal{F}, A), x)
     & = & \swap(\mathsf{decomp}_1(\mathcal{F}, x), A \setminus \{x\}) \cup \remove(\mathsf{decomp}_0(\mathcal{F}, x)).
\end{eqnarray*}
Otherwise $(x \notin A)$,
\begin{eqnarray*}
    \mathsf{decomp}_0(\swap(\mathcal{F}, A), x)
     & = & \swap(\mathsf{decomp}_0(\mathcal{F}, x), A) , \\
     \mathsf{decomp}_1(\swap(\mathcal{F}, A), x)
     & = & \swap(\mathsf{decomp}_1(\mathcal{F}, x), A).
\end{eqnarray*}
\end{lemma}

Our algorithm for $\swap$ is very similar to $\add$.
Therefore, we just show pseudocode for $\swap$ in Algorithm~\ref{alg:swap}.

\begin{algorithm}[t]
\caption{$\swap(\mathcal{F}, A)$}
\label{alg:swap}
\If {$\mathcal{F} = \emptyset$ or $A = \emptyset$}{
    \Return{$\emptyset$}. \\
} \ElseIf {$\mathcal{F} = \{\emptyset\}$}{
    Construct a ZDD $\mathcal{Z}$ representing $\{ \{x\} \mid x \in A \}$ and \Return{$\mathcal{Z}$}. \\
}
$\mathcal{F}_0 \gets \mathsf{child}_0(\mathcal{F})$, $\mathcal{F}_1 \gets \mathsf{child}_1(\mathcal{F})$, $x \gets \labeln(\rootn(\mathcal{F}))$, $y \gets \min(A)$. \\
\If {$x = y$}{
$\mathcal{Y} \gets \swap(\mathcal{F}_0, A \setminus \{x\})$, $\mathcal{Y'} \gets \add(\mathcal{F}_1, A \setminus \{x\})$. \\
$\mathcal{Z}_0 \gets \mathsf{union}(\mathcal{Y}, \mathcal{Y'})$. \\
$\mathcal{Y} \gets \swap(\mathcal{F}_1, A \setminus \{x\})$, $\mathcal{Y'} \gets \remove(\mathcal{F}_0)$. \\
$\mathcal{Z}_1 \gets \mathsf{union}(\mathcal{Y}, \mathcal{Y'})$. \\
$\mathcal{Z} \gets \mathsf{getnode}(x, \mathcal{Z}_0, \mathcal{Z}_1)$. \\
} \ElseIf {$x > y$} {
$\mathcal{Z}_0 \gets \swap(\mathcal{F}, A \setminus \{y\})$, $\mathcal{Z}_1 \gets \remove(\mathcal{F})$. \\
$\mathcal{Z} \gets \mathsf{getnode}(y, \mathcal{Z}_0, \mathcal{Z}_1)$. \\
} \Else {
$\mathcal{Z}_0 \gets \swap(\mathcal{F}_0, A)$, $\mathcal{Z}_1 \gets \swap(\mathcal{F}_1, A)$. \\
$\mathcal{Z} \gets \mathsf{getnode}(x, \mathcal{Z}_0, \mathcal{Z}_1)$. \\
}
\Return{$\mathcal{Z}$}
\end{algorithm}

\begin{algorithm}[t]
\caption{\textsf{FindReconfSequence}($\mathcal{U}, A, S, T$)}
$\mathcal{F}_{-1} \gets \emptyset$, $\mathcal{F}_0 \gets \{S\}$, $i \gets 0$. \\
\While{$\mathcal{F}_i \neq \emptyset$ and $T \notin \mathcal{F}_i$}{
    $\mathcal{F}_{i + 1} \gets \swap(\mathcal{F}_{i}, A) \cap \mathcal{U} \setminus \mathcal{F}_{i - 1}$. \\
    $i \gets i + 1$.
}
\If{$\mathcal{F}_i = \emptyset$}{
    Output ``No sequence from $S$ to $T$.''
} \Else {
    Comment: Here, $T \in \mathcal{F}_i$ holds. \\
    $n \gets i$, $i \gets i - 1$, $I_0 \gets S$, $I_{n} \gets T$. \\
    \While{$i > 0$}{
        Find an independent set $I_i \in \mathcal{F}_{i}$ such that $I_i \bigtriangleup I_{i + 1} = 1$. \\
        $i \gets i - 1$. \\
    }
    Output $I_0, I_1,\ldots,I_n$.
}
\end{algorithm}

\fi

\clearpage

\bibliographystyle{plain}
\bibliography{reference}

\end{document}

\providecommand{\noopsort}[1]{}
\begin{thebibliography}{10}

\bibitem{https://doi.org/10.1002/jgt.22856}
Hugo~A. Akitaya, Matthew~D. Jones, Matias Korman, Oliver Korten, Christopher
  Meierfrankenfeld, Michael~J. Munje, Diane~L. Souvaine, Michael Thramann, and
  Csaba~D. Tóth.
\newblock Reconfiguration of connected graph partitions.
\newblock {\em Journal of Graph Theory}, 102(1):35--66, 2023.

\bibitem{BC09}
Paul Bonsma and Luis Cereceda.
\newblock Finding paths between graph colourings: {PSPACE}-completeness and
  superpolynomial distances.
\newblock {\em Theoretical Computer Science}, 410(50):5215--5226, 2009.

\bibitem{Bryant1986}
Randal~E. Bryant.
\newblock Graph-based algorithms for {B}oolean function manipulation.
\newblock {\em IEEE Transactions on Computers}, C-35(8):677--691, 1986.

\bibitem{Castro2022}
Margarita~P. Castro, Andre~A. Cire, and J.~Christopher Beck.
\newblock Decision diagrams for discrete optimization: A survey of recent
  advances.
\newblock {\em INFORMS Journal on Computing}, 34(4):2271--2295, 2022.

\bibitem{CENSORHILLEL202085}
Keren Censor-Hillel and Mikaël Rabie.
\newblock Distributed reconfiguration of maximal independent sets.
\newblock {\em Journal of Computer and System Sciences}, 112:85--96, 2020.

\bibitem{Cereceda2008}
Luis Cereceda, Jan {\noopsort{Heuvel}van den Heuvel}, and Matthew Johnson.
\newblock Connectedness of the graph of vertex-colourings.
\newblock {\em Discrete Mathematics}, 308(5--6):913--919, 208.

\bibitem{CAV02}
Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia,
  Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella.
\newblock {NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking}.
\newblock In {\em Proc. International Conference on Computer-Aided Verification
  (CAV 2002)}, volume 2404 of {\em LNCS}, Copenhagen, Denmark, July 2002.
  Springer.

\bibitem{582363}
Olivier Coudert.
\newblock Solving graph optimization problems with {ZBDD}s.
\newblock In {\em Proceedings European Design and Test Conference. ED \& TC
  97}, pages 224--228, 1997.

\bibitem{Fifield2020}
Benjamin Fifield, Kosuke Imai, Jun Kawahara, and Christopher~T. Kenny.
\newblock The essential role of empirical validation in legislative
  redistricting simulation.
\newblock {\em Statistics and Public Policy}, 7(1):52--68, 2020.

\bibitem{Hayase1995}
Kazuyoshi Hayase, Kunihiko Sadakane, and Seiichiro Tani.
\newblock Output-size sensitiveness of {OBDD} construction through maximal
  independent set problem.
\newblock In Ding-Zhu Du and Ming Li, editors, {\em Computing and
  Combinatorics}, pages 229--234, Berlin, Heidelberg, 1995. Springer Berlin
  Heidelberg.

\bibitem{Heuvel13}
Jan {\noopsort{Heuvel}van den Heuvel}.
\newblock The complexity of change.
\newblock In Simon~R. Blackburn, Stefanie Gerke, and Mark Wildon, editors, {\em
  Surveys in Combinatorics 2013}, volume 409 of {\em London Mathematical
  Society Lecture No te Series}, pages 127--160. Cambridge University Press,
  2013.

\bibitem{InoueTWKYKTMH14}
Takeru Inoue, Keiji Takano, Takayuki Watanabe, Jun Kawahara, Ryo Yoshinaka,
  Akihiro Kishimoto, Koji Tsuda, Shin{-}ichi Minato, and Yasuhiro Hayashi.
\newblock Distribution loss minimization with guaranteed error bound.
\newblock {\em {IEEE} Trans. Smart Grid}, 5(1):102--111, 2014.

\bibitem{IDHPSUU11}
Takehiro Ito, Erik~D. Demaine, Nicholas J.~A. Harvey, Christos~H.
  Papadimitriou, Martha Sideri, Ryuhei Uehara, and Yushi Uno.
\newblock On the complexity of reconfiguration problems.
\newblock {\em Theoretical Computer Science}, 412(12--14):1054--1065, 2011.

\bibitem{ito_et_al:LIPIcs.MFCS.2022.58}
Takehiro Ito, Yuni Iwamasa, Yasuaki Kobayashi, Yu~Nakahata, Yota Otachi,
  Masahiro Takahashi, and Kunihiro Wasa.
\newblock Independent set reconfiguration on directed graphs.
\newblock In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors, {\em
  47th International Symposium on Mathematical Foundations of Computer Science
  (MFCS 2022)}, volume 241 of {\em Leibniz International Proceedings in
  Informatics (LIPIcs)}, pages 58:1--58:15, Dagstuhl, Germany, 2022. Schloss
  Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik.

\bibitem{iwashita2013efficient}
Hiroaki Iwashita and Shin{-}ichi Minato.
\newblock Efficient top-down {ZDD} construction techniques using recursive
  specifications.
\newblock {\em TCS Technical Reports}, TCS-TR-A-13-69, 2013.

\bibitem{KaminskiMM12}
Marcin Kami\'{n}ski, Paul Medvedev, and Martin Milani\v{c}.
\newblock Complexity of independent set reconfigurability problems.
\newblock {\em Theoretical Computer Science}, 439:9--15, 2012.

\bibitem{Kawahara2017}
Jun Kawahara, Takeru Inoue, Hiroaki Iwashita, and Shin{-}ichi Minato.
\newblock Frontier-based search for enumerating all constrained subgraphs with
  compressed representation.
\newblock {\em IEICE Transactions on Fundamentals of Electronics,
  Communications and Computer Sciences}, E100-A(9):1773--1784, 9 2017.

\bibitem{Kawahara2016}
Jun Kawahara, Toshiki Saitoh, Hirofumi Suzuki, and Ryo Yoshinaka.
\newblock Solving the longest oneway-ticket problem and enumerating letter
  graphs by augmenting the two representative approaches with {ZDD}s.
\newblock In {\em Proc.\ of the Computational Intelligence in Information
  Systems Conference (CIIS 2016)}, volume 532, pages 294--305, 2016.

\bibitem{Kawahara2019}
Jun Kawahara, Toshiki Saitoh, Hirofumi Suzuki, and Ryo Yoshinaka.
\newblock Colorful frontier-based search: Implicit enumeration of chordal and
  interval subgraphs.
\newblock In Ilias Kotsireas, Panos Pardalos, Konstantinos~E. Parsopoulos,
  Dimitris Souravlias, and Arsenis Tsokas, editors, {\em Analysis of
  Experimental Algorithms}, pages 125--141, Cham, 2019. Springer International
  Publishing.

\bibitem{knuth:taocp41}
Donald~E. Knuth.
\newblock {\em {The Art of Computer Programming, Volume 4A, Combinatorial
  Algorithms, Part 1}}.
\newblock Addison-Wesley Professional, 1st edition, March 2011.

\bibitem{Minato1993}
Shin{-}ichi Minato.
\newblock Zero-suppressed {BDD}s for set manipulation in combinatorial
  problems.
\newblock In {\em Proc.\ of the 30th ACM/IEEE design automation conference},
  pages 272--277, 1993.

\bibitem{DBLP:journals/ieicet/MizutaIZ17}
Haruka Mizuta, Takehiro Ito, and Xiao Zhou.
\newblock Reconfiguration of steiner trees in an unweighted graph.
\newblock {\em {IEICE} Trans. Fundam. Electron. Commun. Comput. Sci.},
  100-A(7):1532--1540, 2017.

\bibitem{Nakahata2020}
Yu~Nakahata, Jun Kawahara, Takashi Horiyama, and Shin{-}ichi Minato.
\newblock Implicit enumeration of topological-minor-embeddings and its
  application to planar subgraph enumeration.
\newblock In M.~Sohel Rahman, Kunihiko Sadakane, and Wing-Kin Sung, editors,
  {\em WALCOM: Algorithms and Computation}, pages 211--222, Cham, 2020.
  Springer International Publishing.

\bibitem{Nishimura18}
Naomi Nishimura.
\newblock Introduction to reconfiguration.
\newblock {\em Algorithms}, 11(4):52, 2018.

\bibitem{Sekine1995}
Kyoko Sekine, Hiroshi Imai, and Seiichiro Tani.
\newblock Computing the {Tutte} polynomial of a graph of moderate size.
\newblock In {\em Proceedings of the 6th International Symposium on Algorithms
  and Computation}, pages 224--233, 1995.

\bibitem{DBLP:journals/corr/abs-2208-02495}
Takehide Soh, Yoshio Okamoto, and Takehiro Ito.
\newblock Core challenge 2022: Solver and graph descriptions.
\newblock {\em CoRR}, abs/2208.02495, 2022.

\bibitem{DBLP:conf/aaai/SpeckMN20}
David Speck, Robert Mattm{\"{u}}ller, and Bernhard Nebel.
\newblock Symbolic top-k planning.
\newblock In {\em The Thirty-Fourth {AAAI} Conference on Artificial
  Intelligence, {AAAI} 2020, The Thirty-Second Innovative Applications of
  Artificial Intelligence Conference, {IAAI} 2020, The Tenth {AAAI} Symposium
  on Educational Advances in Artificial Intelligence, {EAAI} 2020, New York,
  NY, USA, February 7-12, 2020}, pages 9967--9974. {AAAI} Press, 2020.

\bibitem{recon}
Volker Turau and Christoph Weyer.
\newblock Finding shortest reconfigurations sequences of independent sets.
\newblock In {\em Core Challenge 2022: Solver and Graph Descriptions}, pages
  3--14, 2022.

\end{thebibliography}