3
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • $\begingroup$ cs.stackexchange.com/questions/111410/… $\endgroup$
    – Yuval Filmus
    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$
    – David Richerby
    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

0

Reset to default

Your Answer

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