# Determine if a graph has exactly 1 cycle using a SAT solver

I have a connected undirected graph whose edges are either enabled or disabled. I want to create a set of clauses that are SAT iff all enabled edges are part of a single loop.

If I assert that each vertex has either 0 or 2 enabled edges, then graphs where all enabled edges are part of a single loop will satisfy the clauses. However, graphs with multiple disjoint loops can will also satisfy those clauses. How can I make sure that only 1 loop graphs satisfy the clauses?

• cs.stackexchange.com/questions/111410/… – Yuval Filmus Jul 6 '19 at 7:55
• Why do you want to do this with a SAT solver? A graph has exactly one cycle iff $|V|-|E|=c-1$ where $c$ is the number of components and you can check that much more easily than with a SAT solver. You have a hammer but not everything is a nail. – David Richerby Jul 6 '19 at 9:36
• @YuvalFilmus Thank you, I think that addresses my issue – Gabe Burke Jul 6 '19 at 18:30
• @DavidRicherby There are several other constraints that I am enforcing at the same time. My goal is to encode puzzles from The Witness as SAT problems. – Gabe Burke Jul 6 '19 at 18:35