Describing a graph property through logical operations 
Let $G$ be a finite, undirected graph (with no parallel edges or self-loops) with $|V(G)| \geq 1$. A $k$-factor $H$ of $G$ is a spanning subgraph of $G$ (with $V(H) = V(G)$) in which every vertex has degree $k$.
Construct a formula $\phi_G$ that is exactly satisfiable when $G$ has a $2$-factor. Describe how we can construct a $2$-factor for $G$ from every interpretation (model) that satisfies $\phi_G$ and how we can construct a model satisfying $\phi_G$ from every $2$-factor for $G$.


What I'm trying to do is describe this $2$-factor property in terms of big conjunctions and disjunctions. For that, I need to define variables and connect them using these conjunctions and disjunctions while imposing the necessary restrictions to obtain a meaningful $\phi_G$. I'm failing at this miserably.
What should the variables stand for and would we begin to construct the formula? I thought about describing the $2$-factor property in predicate logic and then translating it into propositional logic, but I didn't get far there either.
What I do know is that a $1$-factor is just a perfect matching. So if we could somehow obtain a formula for that, the $2$-factor should have a similar structure, but I'm really not sure how to do this or if this the right approach.
Any help would be much appreciated.

EDIT: @HallaSurvivor: Sorry if I'm making this too complicated, but consider this graph:

For vertex $1$, if we had chosen the edge $\{1, 2\}$, then we wouldn't have a $2$-factor, since the cycles aren't disjoint anymore. So how could we know which edges to use from "looking at the graph"? Most of the time (actually always) we don't know what the graph looks like or if it's even connected. For a vertex $x$, the set of all adjacent edges is $\{e_i | x \in e_i \}$. From these edges/variables, we need to find $e_i, e_j$ with $i \neq j$ and set them to true, this would be our $\phi_x$. I'm not sure how to do this. Can you give me a hint or an example for $\phi_x$ for a concrete $x$?
 A: Welcome to MSE!
Hint:
You're looking for a subset of the edges, so you might think of adding a variable $e_i$ for every edge. We want to think of $e_i$ as True whenever we keep it for our 2-factor, and False if we don't. Then every assignment of $e_i$ corresponds to a subgraph, where you keep exactly the edges marked True.
Since you're trying to build a 2-factor, you want to know that every vertex is $2$-regular in the subgraph. So for every vertex $x$, look at its neighbors $\{e_1, \ldots, e_n\}$. You want to write down $\phi_x$ which reads "exactly 2 of $e_1 \ldots e_n$ are True". Can you see how to do that? Importantly we know the graph in advance, so we can "hard code" the $e_i$ that are edges adjacent to $x$.
I then claim that the (finite!) conjunction $\bigwedge_x \phi_x$, is the formula you want. Do you see why?

Edit:
Let's use the graph you showed as an example. I've added labels to the rest of the vertices too.

We'll write $e_{ij}$ for a boolean variable corresponding to an edge connecting $i$ to $j$ (if one exists). Let's always write it with $i < j$ so that we have exactly one variable for every edge.
For example, we will have variables $e_{12}, e_{15}, e_{16}$, but not $e_{13}$, since there is no edge from $1$ to $3$ in the graph.
Now, $\phi_1$ should say "exactly two of the edges touching $1$ are true". We can express this as
$$(e_{12} \land e_{15}) \lor (e_{12} \land e_{16}) \lor (e_{15} \land e_{16})$$

At this point you should stop, and write down $\phi_n$ for all the other $2 \leq n \leq 9$. At least do a few, so that you're convinced you know what's going on.

Ok, now that we have all the $\phi_n$, each of which says "exactly two of my edges are True", we'll conjoin them all:
$$\phi_G = \phi_1 \land \phi_2 \land \ldots \land \phi_9$$
I claim, now, that $\phi_G$ is satisfiable if and only if we can find a $2$-factor in $G$.
Well, we have a $2$-factor in $G$ given to us (it's shown in the picture). If we make the assignment
$$e_{ij} = 
\begin{cases} 
1 & e_{ij} \text{ is used in the $2$ factor} \\
0 & e_{ij} \text{ is NOT used in the $2$ factor}
\end{cases}
$$
Then I claim this assignment makes $\phi_G$ true. Why? Because in a $2$ factor, any vertex sees exactly 2 edges of the 2 factor. That's what a $2$ factor does.

At this point you should check by hand that the assignment shown in the picture actually does make $\phi_G$ true.

Lastly, we want to say that any assignment of the variables which makes $\phi_G$ true will be a $2$ factor. That is, given some assignment of the $e_{ij}$ to $0$ and $1$ which makes $\phi_G = 1$, we claim
$$ \{ e_{ij} \mid e_{ij} \text{ is assigned $1$} \} \text{ is a $2$ factor}$$
Again, the idea is simple:
Every vertex $n$ must see exactly $2$ edges (since that's what $\phi_n$ says, and we know $\phi_n$ is true). So the edges we keep form a $2$ factor.

Convince yourself of this. Maybe try some small examples by hand. I don't think you'll really understand it until you play with it yourself for a while, so make sure you do!


I hope this helps ^_^
