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$ – Yuval Filmus Jul 6 '19 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$ – David Richerby Jul 6 '19 at 9:36
  • $\begingroup$ @YuvalFilmus Thank you, I think that addresses my issue $\endgroup$ – Gabe Burke Jul 6 '19 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 '19 at 18:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.