sambayless / monosat

MonoSAT - An SMT solver for Monotonic Theories
MIT License
106 stars 29 forks source link

Undirected acyclicity constraint bevahiour #21

Closed acairncross closed 4 years ago

acairncross commented 5 years ago

It seems that having any undirected edges in a graph causes it to be cyclic. Is this the intended behaviour/is there another way to express the acyclicity constraint that I want?

>>> from monosat import *
>>> g = Graph()
>>> n1, n2 = [g.addNode() for _ in range(2)]
>>> e1 = g.addUndirectedEdge(n1, n2)
>>> Assert(g.acyclic(directed=False))
>>> Assert(e1)
>>> Solve()
False
sambayless commented 5 years ago

I should improve the documentation about undirected acyclicity. Since under the covers monosat only supports directed edges right now, the undirected acyclicity predicate was implemented somewhat awkwardly.

For the purposes of the undirected acyclicity predicate (and only for that predicate), directed edges are treated as undirected.

Because normally undirected edges are implemented by adding two directed edges in opposite directions, those faux "undirected edges" immediately introduce an undirected cycle, as far as the undirected acyclicity predicate is concerned.

So instead, you should introduce only a single directed edge between each node (in an arbitrary direction). The acyclicity predicate will treat that edge as if it were undirected, and enforce acyclicity over that graph.

On Sun, Jun 23, 2019, 5:24 AM Aiken Cairncross notifications@github.com wrote:

It seems that having any undirected edges in a graph causes it to be cyclic. Is this the intended behaviour/is there another way to express the acyclicity constraint that I want?

from monosat import *>>> g = Graph()>>> n1, n2 = [g.addNode() for _ in range(2)]>>> e1 = g.addUndirectedEdge(n1, n2)>>> Assert(g.acyclic(directed=False))>>> Assert(e1)>>> Solve()False

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/sambayless/monosat/issues/21?email_source=notifications&email_token=AABOECR3J2ZQQGOZZOLJOLLP35TRLA5CNFSM4H2YY7O2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4G3EPOTQ, or mute the thread https://github.com/notifications/unsubscribe-auth/AABOECWPENKKBEFOVYY7QOLP35TRLANCNFSM4H2YY7OQ .

acairncross commented 5 years ago

Ah thanks, that works :+1: