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?

  • $\begingroup$ cs.stackexchange.com/questions/111410/… $\endgroup$ Jul 6, 2019 at 7:55
  • $\begingroup$ 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. $\endgroup$ Jul 6, 2019 at 9:36
  • $\begingroup$ @YuvalFilmus Thank you, I think that addresses my issue $\endgroup$
    – Gabe Burke
    Jul 6, 2019 at 18:30
  • $\begingroup$ @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. $\endgroup$
    – Gabe Burke
    Jul 6, 2019 at 18:35


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.