"Bad solution" error with acyclic property and self edge

[divergentdave]

I ran into the error message below. I minimized a reproducing test case by hand, and it seems to be related to the combination of an acyclic property being asserted, along with a self edge in the GNF. The error is sensitive to other changes as well, presumably because it winds up investigating a good solution first in those cases.

Error in solution of graph theory 0, in detector 0 (Cycle Detector)
Unexpected error:
BAD SOLUTION: failure in graph theory detector

p cnf 12 8
1 0
12 9 0
digraph 3 11 0
edge 0 2 2 9
edge 0 2 1 12
acyclic 0 1

[sambayless]

Thank you for providing a minimized example! That is hugely helpful.

(As an aside - if this happens again, you can use a delta debugger, like this one, to minimize the error automatically).

Is it ok with you if I include this example with the monosat unit tests to catch this issue in the future?

[sambayless]

I've reproduced this error with the provided test case

[sambayless]

Currently, I believe this error applies to any graph with a self-loop edge (from a node to itself). If that turns out to be the case, the fix should be straightforward. Do you have any failing examples without self-loop edges?

[sambayless]

I've pushed a provisional fix to testing branch https://github.com/sambayless/monosat/tree/issue-32

I haven't had enough time to properly verify this change yet or check that it doesn't lead to other errors. If you have a chance to checkout that branch and test it on your example, that would be fantastic.

[divergentdave]

Thanks! I tried out the fix, and it solved the issue on the minimized test case, plus the file I started with before minimizing. Go ahead and include it in the test suite. I haven't run into any similar errors without self-loop edges.

[sambayless]

I've updated unit tests (https://github.com/sambayless/monosat_tests) and merged this change to master. Closing this issue. Thanks again!