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?