Open VeraZhang0311 opened 4 months ago
I tested Formula to find a solution with 3 cycles:
domain Graph { Node ::= new (id: Integer). Edge ::= new (src: Integer, dst: Integer). edgeHasSrc ::= (src: Integer). edgeHasDst ::= (dst: Integer). path ::= (Integer, Integer). cycle ::= (Integer). badSrc ::= (src: Integer). badDst ::= (dst: Integer). edgeHasSrc(a) :- Edge(a, b), Node(a). edgeHasDst(b) :- Edge(a, b), Node(b). badSrc(a) :- Edge(a, b), no edgeHasSrc(a). badDst(b) :- Edge(a, b), no edgeHasDst(b). path(a, b) :- Edge(a, b). path(a, c) :- path(a, b), path(b, c). cycle(a) :- path(a, a). conforms no badSrc(_). conforms no badDst(_). enoughNodes :- count({ n | n is Node(_)}) > 1. conforms enoughNodes. enoughEdges :- count({ e | e is Edge(_, _)}) > 3. conforms enoughEdges. enoughCycles :- count({ c | c is cycle(_)}) = 3. conforms enoughCycles. } partial model pm of Graph [solver_RecursionBound = 10] { Node(t). Node(u). Node(v). Edge(l, m). Edge(n, o). Edge(p, q). Edge(r, s). }
The (incorrect) solution to the partial model is:
Node(7) Node(8) Node(9) Edge(7, 7) Edge(8, 8) Edge(8, 7) Edge(9, 7)
which shouldn't have a cycle(9) but Formula indicates it does.
Potential fix in e67da6595bc3d7d593d2de5891bffb416e8c52ea. Needs testing. Note that setting [solver_RecursionBound = 10] is probably a bit high. It's faster to test with [solver_RecursionBound = 5].
I tested Formula to find a solution with 3 cycles:
The (incorrect) solution to the partial model is:
which shouldn't have a cycle(9) but Formula indicates it does.