"Check if a cycle of K nodes exists" reduction to SAT?

I got the following problem statement:

"Given a undirected graph, check if a cycle of K nodes exists."

And I want to take any input and convert it to a Conjunctive Normal Form formula for SAT solver.

The first step would be creating the variables. We have N variables which represents whether a node is part of the cycle or not, and M variables which would be the same for the edges.

The second part would be formulating constraints via clauses. We would start by adding a constraint "x1 + x2 + ... + xn = k". One method could be creating nCk clauses, which would represent all possible choices. However, I'm struggling to set the rest of constrains to check if the chosen nodes form a cycle.

I've though about recreating all possibilities in DNF and then transform it into CNF, but that would generate too many clauses.

Any suggestions to solve this in CNF form? (Sorry for my english)

We would start by adding a constraint "x1 + x2 + ... + xn = k". One method could be creating nCk clauses, which would represent all possible choices.

Another option is creating a counting circuit (Tseytin transformed) or sorter, then constrain its output to be k. This introduces extra variables.

However, I'm struggling to set the rest of constrains to check if the chosen nodes form a cycle.

I don't know a good way to solve it in that formulation either, but you can change your variables to make it possible to solve that problem without an exponential number of clauses:

• Let x[i,j] indicate whether node i is in position j in the cycle.
• Constrain each node to be used at most once. O(nk²) clauses
• Constrain each position to have exactly one node associated with it. O(kn²) clauses
• Constrain every pair of non-adjacent nodes to not be in position s and s+1 (including wrap-around). O(kn²) clauses